昨日今日と旅行で箱根に行ってきた．旅行は超楽しかったのだけど，2日目の今日から花粉症の症状がひどくてブチ切れている． 僕の花粉症の症状は目のかゆみ，普段より多い目ヤニ，とどまることを知らない鼻水，くしゃみ，口呼吸をしてしまうことからの唇荒れ…

4月に会社員になるにあたって、身元保証書に父の署名をもらうため高崎日帰り旅行した。郵送でも良かったんだけど、直接行って色々話ができて良かった。自分が動けるときは動くといいことがある。 ところで身元保証書って必要なんかね？こんなのあっても気休…

決めた． バックスラッシュとか辛かったから今度手に入れるPCはUSキーボード配列のものにする． 慣れるまで大変そうだけど，そっちの方がなんかかっこいいし．

でも，書くためにリサーチしてたら時間経って書きたくなくなるんだよ． あーあ． 今日書きたかったことは，「LEANファイルをEmacsで編集してるときに 簡単に打ち込める記号一覧の見方」． でも，それをしようとしたときにバックスラッシュ'\'キーで円マーク'…

ちょっと空いた時間にLEANで圏論をやってる． 自然変換の等価性を証明するときに困ったけど，友達に聞いて解決したので備忘録． 結論から言うと， 構造体を要素に分解するときはcases_onを使う． cc tacticは便利． 構造体hogeで説明（？） 次のようにして構…

本業の方の研究が進んだと思った一時間後にダメだったことが判明した。今の方針で進んだ先の反例が分かったという意味は進捗があったが、バックトラックすることになりそう。もー

毎日ブログ書こうと思っていたけど、やりたいことが多くてもう一月近く書けてなかった。よくないなぁ

「微分形式の幾何学」（著：森田茂之）をゆっくり勉強している。 この本の§1.3 (c)の命題1.29の証明で次のような記述がある。 は多様体であるから、もちろん局所コンパクトなHausdorff空間である。 このことからの中でがコンパクトなものだけを集めても 開集…

夢は「リモコン統一」！！ 家の照明がリモコン操作になってから、いろんなところにリモコンがある。 中にはボタンを二度押さないと照明が消えないリモコンもあり、なんとも使いづらい。 そんな折、Raspberry Piで安くリモコンを自作する解説記事を見つけた。…

微分可能多様体の定義について 位相多様体とは 位相空間が次元位相多様体であるとは、 次の三つの性質をすべて満たしていることである。 すなわち、 Hausdorffの分離公理が成り立つ。 第二可算公理が成り立つ。 任意の点に対して、の局所座標系が存在する。 …

全射と商位相 今日は多様体の例を見ていて商位相が出てきたときにふと引っかかったことを書く。 商位相の定義にはいくつか流儀があるかもしれないけど、 例えば以下のように定義される。 定義 を位相空間、を集合、を全射とする。 このとき、のによる商位相…

最近、習慣づけたいことがいくつかあって、下のアプリを使っている。 play.google.com 事柄ごとにウィジェットを作ると、ホーム画面でチェックを入れられる。 便利。 習慣がどの程度達成できているのかも視覚的にわかりやすく表示してくれる。 便利。 ブログ…

背景 「微分形式の幾何学」（著: 森田茂之）という本で勉強をしている。 解析学も位相空間論もちゃんとできてないのにこんなのできるのという不安はあるが、 まあ、数学は自由なのでやってみている。 ところで、この本では位相多様体を定義に第二可算公理を…

以下のツイートが私のTLに流れてきた。 この連ツイは一読推奨。 https://t.co/HkjQrZe1kz— Kontan_Bigcat (@Kontan_Bigcat) 2018年10月10日 確かに一読の価値があるというか、 投稿者サナギさんの危機感を読み取れるツイート群だった。 このツイート群の概略…

微分形式の幾何学を勉強し始めた。 位相空間論も解析学もちゃんと理解できていないのに大丈夫なのだろうか。 案の定、自分で書いた証明が正しいのか判定することすらできず、周りに聞ける人もいないのでLEANで証明を書きたくなった。 人間のチェックなんて信…

今日(2018/09/24)、僕の大好きなバンドBUMP OF CHICKENが『シリウス』をリリースした。 iTunes Storeで購入。 公式サイトによると、他にもいくつかの配信サイトで買えるらしい。 YouTubeにミュージックビデオも公開されている。 感想 まだ3, 4回くらいしか聴…

奈良に来たナラ大仏！ 修学旅行の中学生（に見える人たち）がはしゃいでいて楽しそうだった。 大仏を見て、「でっけぇ！」って叫ぶ若さが10年前にはあったんだなぁ。 クラブツーリズムで来てる中高年（に見える人たち）もはしゃぎはせずとも楽しそうだった。…

台風21号が関西地方に直撃して大変な被害らしい。 僕は東京に住んでて家の中にいれば安全な程度の風なので、家の中でのんびりぷろろうを描こうと思う。 画像のサイズ ツイッターやはてなブログのアイコンとして使おうと思っているので、それに適した画像サイ…

ぷろろう誕生 先日、とある友人に僕のマスコットキャラクターを製作してもらった。 そのマスコットキャラクターがこちら。 名前は僕のハンドルネーム「ぷろろろ」とモチーフとなった「ふくろう」から「ぷろろう」に決まった。 自由に使っていいと言われたの…

スマホで英語の勉強をした気になるために英語物語をプレイしている。これは英語のクイズを解くことで敵を攻撃し、日本全国を行脚するゲームだ。地道に2年くらいプレイして、残るは沖縄と北海道というところまで進んでいた。 しかし、データの引き継ぎをしな…

外見以外で思ったことを書く。 良いところ プレインストールアプリが少ない Essential Phoneの最高に良い点はプレインストールアプリが少ないこと。大体のandroid端末はベンダーの作った使いもしないクラウドサービスやカレンダーアプリ、メールクライアント…

昨日、長野から帰ってくると家にEssencial Phone PH-1が届いていた。 この前注文したやつね。 開封してからずっとワクワクが止まらん。 まだ一日しか使っていないけど、レビューしてきたい。 細かいことは抜きに結論から言うと、スマートフォンの目指す『ス…

そう思いました。

長野県の諏訪にきました。 プログラミングシンポジウム略してプロシンに参加してます。 旅館から見える諏訪湖と夕日 僕は迷路を解くゲルオートマトンについて発表しました。 多くの人には何のこっちゃでしょうが、まあなんとか無事に発表を終えられました。 …

連日のベース練習記事の投稿。 以前にも書いたけど、僕のベースを練習する大目標はジブリ映画「耳をすませば」に出てくる地球屋の爺ちゃんたちのように、 仲間内でセッションをして楽しめるようになることだ。 下の二つの動画を見た結果、タブ譜に頼っていて…

音楽のど素人だから間違ってるかもしれないけど、チューニングについての僕の理解を書く。 チューニングというのは、楽器を弾いたときにちゃんと狙った音を出せるように調整すること。 基準となるAの音が440Hzで、2倍の880Hzが1オクターブ高いAとなるように…

楽譜の入手 ベース練習の目標はBUMP OF CHICKENの「車輪の唄」を弾くことにした。下のリンク先で楽譜が見れる。 車輪の唄 ベース / BUMP OF CHICKEN/バンプ(ベース) 練習で何回も見ると思ってブックマークに加えた。 本当は印刷しておきたいんだけど、サイト…

研究室にベースが持ち込まれた。 ギターよりも低い音が出る弦楽器。 まだ弾き方もよくわからない状態だけど、一応音は出せたのでベーシストとなった。 練習して他の人と合わせて演奏とかできるようになれたら嬉しい。 おっきい目標は、「耳をすませば」に出…

昨日見た裏切りマンキーコングの動画で西澤さんの格言に心を動かされた。 曰く、 ノーチラスというブキが存在しているのに使わないヤツは、 足の速い帰宅部と同じ！ その心は モッタイナイ！ だそうだ。 別に強いわけではないがとにかく面白いらしい。 実際…

SATySFiは2017年度の未踏プロジェクトで開発された組版処理システムで、 「柔軟な記述とわかりやすいエラー報告」が謳われている。 論文執筆するさいにLaTeXのわけわからんエラーで時間を食うんはもう嫌なのでSATySFiを使ってみようと思う。 Gitリポジトリ S…