3段階で考えよう
- モジュラー形式では、対称性で整理した上半平面の境界方向、尖点でのふるまいを制御します。
- カスプ形式では、すべての尖点で適切な極限が0になるという、さらに強い条件を加えます。尖点で0でも、どこでも0とは限りません。
- FLTの後半では、特定の重さとレベルの空間の形式が、どこでも0だと定理で示します。これは追加の結論です。
順番 47 / 64
大学
カスプ形式
モジュラー形式に、すべての尖点で0へ近づく条件を加えたもの。
まず、身近な例で
一歩ごとに半分になる量と、ずっと1のままの量を比べます。先へ進むほど、0へ近づくのはどちらかな？
2回半分にすると0.25。有限回では0そのものになりませんが、0に近づきます。
この例と、本当の定義の違い
半分ずつになる数列は、カスプ形式そのものではありません。本物の尖点は決まった境界の点で、すべての尖点について条件を確かめます。
ちいさな確認：考えてみよう
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
8歩目は1/256 = 0.00390625。「0へ近づく」と「0そのもの」は違います。この数列は模型で、カスプ形式そのものではありません。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ、1/256で、0に近いが0ではない。 8歩目は1/256 = 0.00390625。「0へ近づく」と「0そのもの」は違います。この数列は模型で、カスプ形式そのものではありません。
Leanの定義・原文の抜粋
Mathlib · db584cd · Basic.lean
structure CuspForm extends SlashInvariantForm Γ k whereholo' : MDiff (toSlashInvariantForm : ℍ → ℂ)zero_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c Γ) : c.IsZeroAt toFun k
このLeanの読み方
zero_at_cusps′が尖点で0へ近づく条件を保存します。変換規則を引き継ぎ、holo′の条件も持っています。