Skip to content

Commit cf51696

Browse files
loefflerdloefflerd
committed
order of vanishing stuff
1 parent 39cc630 commit cf51696

File tree

3 files changed

+204
-1
lines changed

3 files changed

+204
-1
lines changed

‎ModularFormDimensions.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,4 @@
11
import ModularFormDimensions.Basic
2+
import ModularFormDimensions.Divisor
3+
import ModularFormDimensions.MathlibPRs.MeromorphicOrder
4+
import ModularFormDimensions.MathlibPRs.ModularFormBounds

‎ModularFormDimensions/Divisor.lean‎

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
/-
2+
Copyright (c) 2025 David Loeffler. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: David Loeffler
5+
-/
6+
7+
import Mathlib.NumberTheory.ModularForms.Cusps
8+
import Mathlib.NumberTheory.ModularForms.Basic
9+
import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
10+
import Mathlib.Algebra.Group.Action.Sum
11+
import Mathlib.Analysis.Meromorphic.Order
12+
import Mathlib.Analysis.Complex.CauchyIntegral
13+
14+
import ModularFormDimensions.MathlibPRs.MeromorphicOrder
15+
16+
17+
open UpperHalfPlane Filter Topology
18+
19+
open scoped ModularForm
20+
21+
private lemma UpperHalfPlane.analyticAt_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
22+
AnalyticAt ℂ (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) τ := by
23+
refine DifferentiableOn.analyticAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.property)
24+
-- surely the following must be proved in mathlib somewhere?
25+
suffices DifferentiableOn ℂ (num g / denom g) _ by
26+
refine this.congr fun z (hz : 0 < z.im) ↦ ?_
27+
simp_all [σ, coe_smul, ofComplex_apply_of_im_pos]
28+
unfold num denom
29+
exact .div (by fun_prop) (by fun_prop) fun _ hz ↦ denom_ne_zero_of_im g hz.ne'
30+
31+
private lemma UpperHalfPlane.deriv_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
32+
deriv (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) τ = g.val.det / denom g τ ^ 2 := by
33+
have : (fun z ↦ ↑(g • ofComplex z)) =ᶠ[𝓝 ↑τ] (num g / denom g) := by
34+
filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds τ.im_pos] with z hz
35+
simp [coe_smul, ofComplex_apply_of_im_pos hz, σ, if_pos hg]
36+
rw [EventuallyEq.deriv_eq this,
37+
deriv_div (by unfold num; fun_prop) (by unfold denom; fun_prop) (denom_ne_zero g τ)]
38+
congr 1
39+
unfold num denom
40+
simp only [deriv_add_const, Matrix.det_fin_two]
41+
-- why does `rw` work here but `simp` does not?
42+
rw [deriv_const_mul_field, deriv_id'', deriv_const_mul_field, deriv_id'']
43+
push_cast
44+
ring
45+
46+
private lemma UpperHalfPlane.deriv_smul_ne_zero {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
47+
deriv (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) τ ≠ 0 := by
48+
rw [deriv_smul hg]
49+
apply div_ne_zero
50+
· exact_mod_cast hg.ne'
51+
· exact pow_ne_zero _ (denom_ne_zero g τ)
52+
53+
private lemma order_comp_smul {f : ℍ → ℂ} {τ : ℍ} {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) :
54+
meromorphicOrderAt (fun z ↦ f (g • ofComplex z)) τ =
55+
meromorphicOrderAt (fun z ↦ f (ofComplex z)) ↑(g • τ) := by
56+
let G z : ℂ := ↑(g • ofComplex z)
57+
let F z := f (ofComplex z)
58+
have : (fun z : ℂ ↦ f (g • ofComplex z)) = F ∘ G := by ext; simp [F, G]
59+
rw [this, meromorphicOrderAt_comp_of_deriv_ne_zero]
60+
· simp [F, G]
61+
· exact τ.analyticAt_smul hg
62+
· exact τ.deriv_smul_ne_zero hg
63+
64+
open scoped ModularForm in
65+
private lemma order_slash {k : ℤ} {f : ℍ → ℂ} {τ : ℍ} {g : GL (Fin 2) ℝ}
66+
(hg : 0 < g.val.det) :
67+
meromorphicOrderAt (fun z : ℂ ↦ (f ∣[k] g) (ofComplex z)) ↑τ =
68+
meromorphicOrderAt (fun z ↦ f (ofComplex z)) ↑(g • τ) := by
69+
simp only [ModularForm.slash_def, σ, Matrix.GeneralLinearGroup.val_det_apply, hg, ↓reduceIte,
70+
RingHom.id_apply, zpow_neg, mul_assoc, ← order_comp_smul hg]
71+
rw [← Pi.mul_def, mul_comm, meromorphicOrderAt_mul_of_ne_zero]
72+
· refine .const_smul (.inv ?_ ?_)
73+
· refine .fun_zpow ?_ (denom_ne_zero g _)
74+
refine (analyticAt_id.congr ?_).const_smul.add analyticAt_const
75+
filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds τ.im_pos] with z hz
76+
simp [ofComplex_apply_of_im_pos hz]
77+
· exact zpow_ne_zero _ <| denom_ne_zero g _
78+
· apply mul_ne_zero
79+
· norm_cast
80+
positivity
81+
· rw [Ne, inv_eq_zero]
82+
exact zpow_ne_zero _ <| denom_ne_zero g _
83+
84+
variable (𝒢 : Subgroup (GL (Fin 2) ℝ))
85+
86+
/-- The quotient `𝒢 \ ℍ`, where `𝒢` is a subgroup of `GL(2, ℝ)`. -/
87+
def OpenModularCurve : Type := MulAction.orbitRel.Quotient 𝒢 ℍ
88+
89+
local notation "Y(" 𝒢 ")" => OpenModularCurve 𝒢
90+
91+
/-- Order of vanishing of a meromorphic `SlashInvariantForm`.
92+
93+
TODO: Is this the morally right definition? Do we want to `weight` it by
94+
the order of the stabilizer (at a cost of being `ℚ∞`-valued)? -/
95+
noncomputable def meromorphicOrderQuotient {k : ℤ} (f : SlashInvariantForm 𝒢 k)
96+
[𝒢.HasDetOne] : Y(𝒢) → WithTop ℤ :=
97+
Quotient.lift (meromorphicOrderAt (f ∘ ofComplex) ·) (by
98+
rintro _ b ⟨⟨g, hg⟩, rfl⟩
99+
dsimp only [Subgroup.smul_def, Function.comp_def]
100+
rw [← order_slash, SlashInvariantFormClass.slash_action_eq f g hg]
101+
have := Units.val_eq_one.mpr <| Subgroup.HasDetOne.det_eq hg
102+
simp_all)
103+
104+
@[simp]
105+
lemma meromorphicOrderQuotient_mk [𝒢.HasDetOne] {k : ℤ} (f : SlashInvariantForm 𝒢 k) (τ : ℍ) :
106+
meromorphicOrderQuotient 𝒢 f ⟦τ⟧ = meromorphicOrderAt (fun z ↦ f (ofComplex z)) ↑τ := by
107+
rfl
108+
109+
/-- The quotient `𝒢 \ ℍ⋆`, where `𝒢` is a subgroup of `GL(2, ℝ)` and `ℍ⋆` denotes the union of
110+
`ℍ` and the cusps of `𝒢`. -/
111+
def CompletedModularCurve : Type := (OpenModularCurve 𝒢) ⊕ CuspOrbits 𝒢

‎ModularFormDimensions/MathlibPRs/MeromorphicOrder.lean‎

Lines changed: 90 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
import Mathlib.Analysis.Meromorphic.Order
22
import Mathlib.Analysis.Calculus.Deriv.Mul
33
import Mathlib.Analysis.Calculus.Deriv.Pow
4+
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
5+
import Mathlib.Analysis.Complex.CauchyIntegral
46

57
/-!
68
# Mathlib PR #33000: analytic order of a composition
@@ -104,11 +106,98 @@ lemma MeromorphicAt.meromorphicOrderAt_comp_of_deriv_ne_zero
104106
rw [hf.meromorphicOrderAt_comp hg, hgo] <;>
105107
simp [eventuallyConst_iff_analyticOrderAt_sub_eq_top, hgo]
106108

109+
/-- If `g` is analytic at `x`, and `g' x ≠ 0`, then the meromorphic order of
110+
`f ∘ g` at `x` is the meromorphic order of `f` at `g x` (even if `f` is not meromorphic). -/
111+
lemma meromorphicOrderAt_comp_of_deriv_ne_zero (hg : AnalyticAt 𝕜 g x) (hg' : deriv g x ≠ 0)
112+
[CompleteSpace 𝕜] [CharZero 𝕜] :
113+
meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x) := by
114+
by_cases hf : MeromorphicAt f (g x)
115+
· exact hf.meromorphicOrderAt_comp_of_deriv_ne_zero hg hg'
116+
· rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
117+
contrapose! hf
118+
-- The remainder of this proof is showing that analytic functions with nonzero derivative
119+
-- have analytic inverses. TODO: extract this into a self-contained lemma.
120+
have hgd : HasStrictDerivAt g (deriv g x) x := by
121+
refine hasStrictDerivAt_iff_hasStrictFDerivAt.mpr ?_
122+
convert hg.hasStrictFDerivAt using 1
123+
ext
124+
simp
125+
have hgfd : HasStrictFDerivAt g
126+
(((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 _ hg'))).toContinuousLinearMap
127+
x := hgd
128+
let R := hgfd.toOpenPartialHomeomorph _
129+
have hx : x ∈ R.source := HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source _
130+
have hra : AnalyticAt 𝕜 R.symm (g x) := by
131+
refine (R.hasFPowerSeriesAt_symm hx hg.hasFPowerSeriesAt
132+
(i := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (.mk0 _ hg')) ?_).analyticAt
133+
ext
134+
simp
135+
have hrne : deriv R.symm (g x) ≠ 0 := by
136+
simpa [(hgd.to_local_left_inverse hg' (R.eventually_left_inverse hx)).hasDerivAt.deriv]
137+
apply (((R.left_inv hx) ▸ hf).comp_analyticAt hra).congr
138+
exact .fun_comp ((R.eventually_right_inverse' hx).filter_mono nhdsWithin_le_nhds) f
139+
107140
/-- If `g` is analytic at `x`, `f` is meromorphic at `g x`, and `g' x ≠ 0`, then the order of
108141
`f ∘ g` at `x` is the order of `f` at `g x`. -/
109-
lemma AnalyticAt.analyticOrderAt_comp_of_deriv_ne_zero {g : 𝕜 → 𝕜}
142+
lemma AnalyticAt.analyticOrderAt_comp_of_deriv_ne_zero
110143
(hf : AnalyticAt 𝕜 f (g x)) (hg : AnalyticAt 𝕜 g x) (hg' : deriv g x ≠ 0) :
111144
analyticOrderAt (f ∘ g) x = analyticOrderAt f (g x) := by
112145
simp [hf.analyticOrderAt_comp hg, hg.analyticOrderAt_sub_eq_one_of_deriv_ne_zero hg']
113146

147+
/-- If `g` is analytic at `x` and `g' x ≠ 0`, then the order of `f ∘ g` at `x` is the order of `f`
148+
at `g x` (even if `f` is not analytic). -/
149+
lemma analyticOrderAt_comp_of_deriv_ne_zero [CompleteSpace 𝕜] [CharZero 𝕜]
150+
(hg : AnalyticAt 𝕜 g x) (hg' : deriv g x ≠ 0) :
151+
analyticOrderAt (f ∘ g) x = analyticOrderAt f (g x) := by
152+
by_cases hf : AnalyticAt 𝕜 f (g x)
153+
· exact hf.analyticOrderAt_comp_of_deriv_ne_zero hg hg'
154+
· rw [analyticOrderAt_of_not_analyticAt hf, analyticOrderAt_of_not_analyticAt]
155+
contrapose! hf
156+
-- The remainder of this proof is showing that analytic functions with nonzero derivative
157+
-- have analytic inverses. TODO: extract this into a self-contained lemma.
158+
have hgd : HasStrictDerivAt g (deriv g x) x := by
159+
refine hasStrictDerivAt_iff_hasStrictFDerivAt.mpr ?_
160+
convert hg.hasStrictFDerivAt using 1
161+
ext
162+
simp
163+
have hgfd : HasStrictFDerivAt g
164+
(((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 _ hg'))).toContinuousLinearMap
165+
x := hgd
166+
let R := hgfd.toOpenPartialHomeomorph _
167+
have hx : x ∈ R.source := HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source _
168+
have hra : AnalyticAt 𝕜 R.symm (g x) := by
169+
refine (R.hasFPowerSeriesAt_symm hx hg.hasFPowerSeriesAt
170+
(i := (ContinuousLinearEquiv.unitsEquivAut 𝕜) (.mk0 _ hg')) ?_).analyticAt
171+
ext
172+
simp
173+
have hrne : deriv R.symm (g x) ≠ 0 := by
174+
simpa [(hgd.to_local_left_inverse hg' (R.eventually_left_inverse hx)).hasDerivAt.deriv]
175+
apply (((R.left_inv hx) ▸ hf).comp hra).congr
176+
exact .fun_comp (R.eventually_right_inverse' hx) f
177+
178+
lemma meromorphicAt_smul_iff_of_ne_zero (hg : AnalyticAt 𝕜 g x) (hg' : g x ≠ 0) :
179+
MeromorphicAt (g • f) x ↔ MeromorphicAt f x := by
180+
refine ⟨fun hfg ↦ ?_, hg.meromorphicAt.smul⟩
181+
refine (hg.inv hg').meromorphicAt.smul hfg |>.congr ?_
182+
filter_upwards [(hg.continuousAt.mono_left nhdsWithin_le_nhds).eventually_ne hg'] with z hz
183+
simp [inv_smul_smul₀ hz]
184+
185+
lemma meromorphicOrderAt_smul_of_ne_zero (hg : AnalyticAt 𝕜 g x) (hg' : g x ≠ 0) :
186+
meromorphicOrderAt (g • f) x = meromorphicOrderAt f x := by
187+
by_cases hf : MeromorphicAt f x
188+
· simp [meromorphicOrderAt_smul hg.meromorphicAt hf, hg.meromorphicOrderAt_eq,
189+
hg.analyticOrderAt_eq_zero.mpr hg']
190+
· rw [meromorphicOrderAt_of_not_meromorphicAt hf, meromorphicOrderAt_of_not_meromorphicAt]
191+
rwa [meromorphicAt_smul_iff_of_ne_zero hg hg']
192+
193+
194+
lemma meromorphicAt_mul_iff_of_ne_zero {f : 𝕜 → 𝕜} (hg : AnalyticAt 𝕜 g x) (hg' : g x ≠ 0) :
195+
MeromorphicAt (g * f) x ↔ MeromorphicAt f x :=
196+
meromorphicAt_smul_iff_of_ne_zero hg hg'
197+
198+
lemma meromorphicOrderAt_mul_of_ne_zero {f : 𝕜 → 𝕜} (hg : AnalyticAt 𝕜 g x) (hg' : g x ≠ 0) :
199+
meromorphicOrderAt (g * f) x = meromorphicOrderAt f x :=
200+
meromorphicOrderAt_smul_of_ne_zero hg hg'
201+
202+
114203
end comp

0 commit comments

Comments
 (0)