q-expansions of modular forms (project-local extensions)

The bulk of the original ForMathlib/QExpansion.lean file has been upstreamed into Mathlib.NumberTheory.ModularForms.QExpansion and Mathlib.Analysis.Complex.CauchyIntegral. This file now only keeps the project-local variants that are parameterised by Γ.width ∣ h rather than h ∈ Γ.strictPeriods, which the rest of the project still uses.

theorem SlashInvariantFormClass.periodic_comp_ofComplex' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {h : ℕ} (f : F) [hF : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (hΓ : Γ.width ∣ h) : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑h

theorem SlashInvariantFormClass.eq_cuspFunction' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {h : ℕ} (f : F) [hF : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] {τ : UpperHalfPlane} [NeZero h] (hΓ : Γ.width ∣ h) : UpperHalfPlane.cuspFunction (↑h) (⇑f) (Function.Periodic.qParam ↑h ↑τ) = f τ

theorem ModularFormClass.differentiableAt_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : F) [hF : ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] {z : ℂ} (hz : 0 < z.im) : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) z

Differentiability of ⇑f ∘ ofComplex at a point with positive imaginary part, recovering the former ModularFormClass.differentiableAt_comp_ofComplex from the manifold-differentiability of a modular form.

theorem ModularFormClass.differentiableAt_cuspFunction' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {h : ℕ} (f : F) {q : ℂ} [hF : ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] [NeZero h] (hΓ : Γ.width ∣ h) (hc : IsCusp OnePoint.infty (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ)) (hq : ‖q‖ < 1) : DifferentiableAt ℂ (UpperHalfPlane.cuspFunction ↑h ⇑f) q

theorem UpperHalfPlane.IsZeroAtImInfty.zeroAtFilter_comp_ofComplex {α : Type u_2} [Zero α] [TopologicalSpace α] {f : UpperHalfPlane → α} (hf : IsZeroAtImInfty f) : (Filter.comap Complex.im Filter.atTop).ZeroAtFilter (f ∘ ↑ofComplex)

theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty_of_width_dvd {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {h : ℕ} {f : F} [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (hf : IsZeroAtImInfty ⇑f) (hΓ : Γ.width ∣ h) : ⇑f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / ↑h)

A modular form which vanishes at the cusp ∞ actually must decay at least as fast as Real.exp (-2 * π * τ.im / n), if n divides the cusp with.

(Note that Γ need not be finite index here).

theorem ModularFormClass.hasFPowerSeries_cuspFunction {F : Type u_2} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : HasFPowerSeriesOnBall (UpperHalfPlane.cuspFunction h ⇑f) (UpperHalfPlane.qExpansionFormalMultilinearSeries h f) 0 1

Recovers the former ModularFormClass.hasFPowerSeries_cuspFunction: the q-expansion of a modular form is an FPowerSeries representing its cuspFunction, derived from the modular-form instance (analyticity at 0 plus the q-expansion HasSum).