funlean.
順番 43 / 64

大学

モジュラー形式

複素数を返し、変換と滑らかさについて厳密な規則を持つ関数。

まず、身近な例で

関数は「数を入れると数が出る仕組み」です。「反対の数を入れても同じ値」という規則なら、x²は合格。2²も(−2)²も4です。xを動かして比べよう。

(2)² = (−2)² = 4

この例と、本当の定義の違い

ここでのx²はモジュラー形式ではありません。「規則を守る関数」の例です。本物は複素数の入力、決まった変換、滑らかさや端での条件を使います。

ちいさな確認：考えてみよう

問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。

模型の関数x²に2と−2を入れると？

答えと考え方を読む

どちらも4。 2×2 = 4、(−2)×(−2) = 4。簡単な対称性の規則の例です。ここでのx²がモジュラー形式だという意味ではありません。

3段階で考えよう

  1. 上半平面の点から複素数を返す関数を用意します。それだけではモジュラー形式ではありません。
  2. 数を2×2に並べた表を行列と呼び、それで点の動かし方を表します。許す動かし方を選び、動かす前後の関数の値に厳密な規則を求めます。その規則に入る数を「重さ」と呼びます。
  3. さらに、点を少し動かしたときの変化の割合が、複素数のどの方向から近づいても同じになること（微分可能性）を求めます。境界へ近づく方向である尖点では、適切に変換した関数が際限なく大きくならないことも必要です。

小さな例で確かめる

奏者は資格を備えた関数の役。心地よい曲はたとえで、実際の要求は表示した定義の欄です。

Leanの定義・原文の抜粋

Mathlib · db584cd · Basic.lean

structure ModularForm extends SlashInvariantForm Γ k where  holo' : MDiff (toSlashInvariantForm : ℍ → ℂ)  bdd_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsBoundedAt toFun k

このLeanの読み方

extends SlashInvariantFormが変換規則を引き継ぎます。holo′は複素微分可能性、bdd_at_cusps′は各尖点で有界にふるまう条件です。

元の原文 ↗ · L75–77保存した原文全体を開く

この言葉を使う章

8. ひみつの二重奏9. コンサートへの二つの入口10. 3音だけのオーディション11. パスポートを借りる作戦12. 二つの工房、同じ注文13. ピップの無謀なキルト14. どんどん小さくなる予約15. 完全なる静寂のコンサート16. 入れないはずの客
わからない・道に迷った

ミカのたすけ舟

モジュラー形式

今は、一つだけ

まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。

言葉をほどこう

複素数を返し、変換と滑らかさについて厳密な規則を持つ関数。

このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。

小さな手がかり

奏者は資格を備えた関数の役。心地よい曲はたとえで、実際の要求は表示した定義の欄です。

閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。

最初の小さな物語から読む →