LEANも数学もよくわからんなぁ
微分形式の幾何学を勉強し始めた。 位相空間論も解析学もちゃんと理解できていないのに大丈夫なのだろうか。 案の定、自分で書いた証明が正しいのか判定することすらできず、周りに聞ける人もいないのでLEANで証明を書きたくなった。 人間のチェックなんて信用できない。まして自分のチェックをや。
ところが、LEANのライブラリは当然そんなに充実していなくて位相やら微分やらの定義から自分でやる必要がありそう。 それに、LEAN標準ライブラリの集合はどんな集合論に基づいているのかよくわからなくて困る。 Reference manualの標準ライブラリの章を早く書いて欲しい。
あと、もっと基本的なこととして、
のとき、
と
から
を導くのが難しい。
友人曰く、これはη変換に関係があるらしい。
勉強することが多くて楽しい。
BUMP OF CHICKENの新曲『シリウス』がリリースされたので聴いてみた
今日(2018/09/24)、僕の大好きなバンドBUMP OF CHICKENが『シリウス』をリリースした。 iTunes Storeで購入。 公式サイトによると、他にもいくつかの配信サイトで買えるらしい。 YouTubeにミュージックビデオも公開されている。
感想
まだ3, 4回くらいしか聴いていない時点での感想。
感動はしなかった。BUMP OF CHICKENの曲はたくさん聴いてるうちにふと心に刺さることがよくあるからそのパターンを期待。 僕は彼らより13歳年下だから、13年後40手前くらいの年齢になって共感しやすいはず。
曲の雰囲気（曲調？）は『Hello, world!』に似ている感じがした。 激しめで音が多いところとか、一瞬音が止まって一斉に入る演出とか。 ジャケットも『Hello, world!』に似ている。 お風呂で歌うのにいいかもしれない。
何回か聴いて気になった歌詞
気になった歌詞となんで気になったのかをメモ。 引用している歌詞は藤原基央さん作。 順番はごちゃごちゃ。 誤りがあるかも。
その心で選んで その声で叫んで
一番好きなものを その手で離さないで
「素直に、自分の心に従って」というような意味だと思う。 『GO』とか『夢の飼い主』のテーマに通じているメッセージなのかな。 『GO』では心が産んだ宝石に名前をつけて空に浮かべていたから、そのなかで一番輝く宝石が「シリウス」？
名前さえ忘れても 何度でも呼んで
って歌詞もやはり『GO』や『夢の飼い主』を連想させる。 そう考えると、「一番好きなもの」=「夢」=「シリウス」なのかな。
名前さえ忘れても 消えない灯火
ってフレーズもあった。 こっちは「灯火」が『ランプ』とか『sailing day』、『ゼロ』を連想させる。
記憶は後ろから削れていく 拾ったものも砂になって落ちる
記憶の「後ろ」ってどっち側だろう？昔？最近？ 「削れていく」「砂になって落ちる」って表現は抗えない風化を感じさせて少し怖い。 まだはっきりわからないけど、「名前さえ忘れても」のフレーズと繋がるのかな。
隔たりを砕いて どうぞ行っておいで
「隔たり」は『虹を待つ人』に出てきた「見えない壁」？ 『太陽』や『トーチ』の部屋も同じ「隔たり」でできてるような気がする。
絶望の最果て 希望の底
つい最近の曲『望遠のマーチ』でも絶望と希望がキーワードになっていた。 この辺は意味がよくわかっていない感がある。 パンドラの箱を連想するような言葉だけど、やっぱりどういうメッセージなのかわからない。
透明な思いの盾と剣
『66号線』で音符を繋いで作った盾と、音符を鍛えて作った剣を連想した。 でも、こっちの盾と剣は自分の心から作ってるけど、『66号線』の方はあなた（恋人？）由来の盾と剣だから別物かも。
それと、ところどころ出てくる「鏡」「約束」「ただいま おかえり」などのフレーズは自分の分身と約束して一度別れ、再開する『カルマ』や『arrows』ぽい。
フューチャーワーク
まあ、いろいろ他の曲と繋がりがありそうだからゆっくり紐解いて行きたい。 それと、『シリウス』はアニメ『重神機パンドーラ』の主題歌なのでそのアニメを観た方が曲の理解が深まるかもしれない。
今日こそぷろろうを描こう
台風21号が関西地方に直撃して大変な被害らしい。 僕は東京に住んでて家の中にいれば安全な程度の風なので、家の中でのんびりぷろろうを描こうと思う。
画像のサイズ
ツイッターやはてなブログのアイコンとして使おうと思っているので、それに適した画像サイズを調べた。 下のサイトによると、ツイッターアイコンには400×400ピクセルが望ましいらしい。
ツイッターのアイコン画像サイズって？かんたんに作成・変更する方法まとめ【twitterプロフィール】 | 毎日が生まれたて
GIMPの使い方がわからん
先日インストールしたGIMPを使おうと、開いてみたら色々ボタンが並んでいて難しそうである。
よくわからなくて色々なサイトを見て回りつつ描いていく。 重要そうなことをまとめると、
- 画像はレイヤーを重ねて作成する。
- 各レイヤーにはチャンネルが設定される。たぶん、チャンネルは画素の標準基底なんだと思う。
- アルファチャンネルというチャンネルを設定すると、透過する画素を作れる。
- 描画はパスや選択範囲を通じて行う。（使い分けはわからない）
といったところ。
元の画像の上に背景が透明なレイヤーを重ねて描いて、あとから元の画像のレイヤーを消せばいい感じにできそう。
と思ったが、右翼の線（画像の赤く表示されたパス）を描こうとしても全然線が出て来てくれない。 何かの設定が間違っているんだと思うけど全く見当がつかない。 今日はここでやめる。
お絵かきソフトも難しいものだなぁ。
マスコットキャラクター「ぷろろう」を描こう
ぷろろう誕生
先日、とある友人に僕のマスコットキャラクターを製作してもらった。 そのマスコットキャラクターがこちら。
名前は僕のハンドルネーム「ぷろろろ」とモチーフとなった「ふくろう」から「ぷろろう」に決まった。 自由に使っていいと言われたので自由に使い倒す。ありがてぇなぁ。
とりあえず、TwitterとFacebookのアイコンをぷろろうに変更した。 何も設定してなくて味気ないはてなブログのアイコンもぷろろうにしようと思ったけど、ちょっと保留。 色をつけるとか、線を太くするとかして完成度をあげてからアイコンにしよう。
お絵かきソフトGIMP
普段絵を描くことは全然ないので、今使っているMac Bookにはお絵かきソフトが入っていない。 とりあえずフリーのお絵かきソフトを探してみると、FireAlpacaやGIMPなどのソフトがあることがわかった。
【無料】2018年最新版！おすすめお絵描きソフト比較【有料】 | イラスト・マンガ描き方ナビ
中でもGIMPは拡張性が高いらしく、僕の好みな気がするのでGIMPをインストールした。 ダウンロードページを見ると、Homebrewでインストールできるらしい。 インストール時間は長め。 というか、インストール始めてからこの記事を書いていたらここまで来てしまってなお34%しかダウンロードが進んでいない。 ネットワークの状況が悪いのかもしれない。
あまりにもインストールに時間がかかるので今日は寝て、また今度絵を描こう。
英語物語のデータ消えた
スマホで英語の勉強をした気になるために英語物語をプレイしている。これは英語のクイズを解くことで敵を攻撃し、日本全国を行脚するゲームだ。地道に2年くらいプレイして、残るは沖縄と北海道というところまで進んでいた。
しかし、データの引き継ぎをしないまま前のスマホからアンインストールした結果、データが消えた。Google Playがデータ管理してくれてると勝手に勘違いしていた。残念だがまた最初からプレイして行く。
最初に貰えるレアキャラは有砂小町２ＰCだった。これからよろしくな。
essential phoneの良いところ悪いところ
外見以外で思ったことを書く。
良いところ
プレインストールアプリが少ない
Essential Phoneの最高に良い点はプレインストールアプリが少ないこと。大体のandroid端末はベンダーの作った使いもしないクラウドサービスやカレンダーアプリ、メールクライアントなど、不要なアプリが最初からインストールされている気がする。僕が使ったことのあるスマホは2台中2台がそうだった。Essential Phoneにプレインストールされていたアプリはカメラや設定などの本体を使う上で必要なアプリと、androidなら必ず入ってるようなグーグル謹製のアプリだけだった。使わないのにアンインストールできない苛立ちから解放される。
安心の技適マーク
日本でも安心して使える技適マークがついている。これは、［設定］>［システム］>［端末情報］>［規制ラベル］と進めば見られる。法律準拠だいじ。pixelとかはその辺が不安で手が出なかった。
OSがAndroid 9
OSが新しいのはいいよね。Andoroid 9は画面下のボタンたちがだいぶ大きく変更されてて、よりスマートになっている。ただ、これは覚えることも多くて馴れが必要かも。僕はすぐ馴れたけど、親とか祖父母世代のスマホが苦手な人には直感的じゃなくて使いづらいかもしれない。
高性能なハードウェア
注文するときも確認したことだけど、8コアのCPUと4GBのRAMは僕の使い方なら十分なスペック。2日間しか使ってないけど、今のところ反応が遅かったりフリーズしたりということはなく快適に使えている。
画面が広い
これは外見としても言及したけど、感動したからもう一度言う。インカメで抉れた並びに時刻や通知が表示されて、有効な画面がとても広く感じる。めちゃくちゃ快適。
ラインモバイルでも使える
個人的に心配してたのが、いま契約しているラインモバイルで使えるかどうかだった。ラインモバイルの公式には動作確認されていなくて実際に使うまで不安だった。アクセスポイントの設定を手動でする必要があったけど、まあ普通に電話もモバイル回線も使えている。
端子がUSB type-c
これは人によってはマイナスポイントかも。僕は新し目のMac Bookを使っていて、USBはtype-bから移行していきたいと思っていたのでプラス。充電やパソコンに繋いだときの通信が速くなってるといいなぁ。
悪いところ
パソコンに繋ぐと、パソコンの充電を始める
充電しようと思って繋いでたら逆にバッテリーを消費した。もうちょっと賢くどちらの方が電力を必要としているのか判断してほしい。
利用規約が英語
いっちばん最初の設定は英語読めないときついと思う。利用規約が何となくしか読めなかったのがちょっと不安。13歳未満の子供は使えないこととか利用規約読むまで知らなかった。
そんなもんかな。全体としては正当なスマートフォンって感じで大好き。
