QExpansionLems

theorem modform_tendto_ndhs_zero {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) {k : ℤ} (n : ℕ) [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k] [inst : NeZero n] : Filter.Tendsto (fun (x : ℂ) => (⇑f ∘ ↑UpperHalfPlane.ofComplex) (Function.Periodic.invQParam (↑n) x)) (nhdsWithin 0 {0}ᶜ) (nhds (UpperHalfPlane.cuspFunction (↑n) (⇑f) 0))

theorem derivWithin_mul2 (f g : ℂ → ℂ) (s : Set ℂ) (hf : DifferentiableOn ℂ f s) (hd : DifferentiableOn ℂ g s) : s.domRestrict (derivWithin (fun (y : ℂ) => f y * g y) s) = s.domRestrict (derivWithin f s * g + f * derivWithin g s)

theorem iteratedDerivWithin_mul' (f g : ℂ → ℂ) (s : Set ℂ) (hs : IsOpen s) (x : ℂ) (hx : x ∈ s) (m : ℕ) (hf : ContDiffOn ℂ ⊤ f s) (hg : ContDiffOn ℂ ⊤ g s) : iteratedDerivWithin m (f * g) s x = ∑ i ∈ Finset.range m.succ, ↑(m.choose i) * iteratedDerivWithin i f s x * iteratedDerivWithin (m - i) g s x

theorem iteratedDeriv_eq_iteratedDerivWithin (n : ℕ) (f : ℂ → ℂ) (s : Set ℂ) (hs : IsOpen s) (z : ℂ) (hz : z ∈ s) : iteratedDeriv n f z = iteratedDerivWithin n f s z

theorem qExpansion_mul_coeff (n : ℕ) (a b : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) a) (g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) b) [hn : NeZero n] : UpperHalfPlane.qExpansion ↑n ⇑(f.mul g) = UpperHalfPlane.qExpansion ↑n ⇑f * UpperHalfPlane.qExpansion ↑n ⇑g

theorem IteratedDeriv_smul (a : ℂ) (f : ℂ → ℂ) (m : ℕ) : iteratedDeriv m (a • f) = a • iteratedDeriv m f

theorem qExpansion_smul2 {k : ℤ} (n : ℕ) (a : ℂ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k) [NeZero n] : a • UpperHalfPlane.qExpansion ↑n ⇑f = UpperHalfPlane.qExpansion (↑n) (a • ⇑f)

@[instance_reducible]

instance instFunLikeUpperHalfPlaneFun : FunLike (UpperHalfPlane → ℂ) UpperHalfPlane ℂ

Equations

• instFunLikeUpperHalfPlaneFun = { coe := fun ⦃a₁ : UpperHalfPlane → ℂ⦄ => a₁, coe_injective := ⋯ }

theorem qExpansion_ext (f g : UpperHalfPlane → ℂ) (h : f = g) : UpperHalfPlane.qExpansion 1 f = UpperHalfPlane.qExpansion 1 g

theorem cuspFunction_congr_funLike {α : Type u_4} {β : Type u_5} [FunLike α UpperHalfPlane ℂ] [FunLike β UpperHalfPlane ℂ] (n : ℕ) (f : α) (g : β) (h : ⇑f = ⇑g) : UpperHalfPlane.cuspFunction ↑n ⇑f = UpperHalfPlane.cuspFunction ↑n ⇑g

theorem qExpansion_ext2 {α : Type u_4} {β : Type u_5} [FunLike α UpperHalfPlane ℂ] [FunLike β UpperHalfPlane ℂ] (f : α) (g : β) (h : ⇑f = ⇑g) : UpperHalfPlane.qExpansion 1 ⇑f = UpperHalfPlane.qExpansion 1 ⇑g

theorem IteratedDeriv_zero_fun (n : ℕ) (z : ℂ) : iteratedDeriv n (fun (x : ℂ) => 0) z = 0

theorem iteratedDeriv_const_eq_zero (m : ℕ) (hm : 0 < m) (c : ℂ) : (iteratedDeriv m fun (x : ℂ) => c) = fun (x : ℂ) => 0

theorem qExpansion_pow {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (n : ℕ) : UpperHalfPlane.qExpansion 1 ⇑(((DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) k) f ^ n) (↑n * k)) = UpperHalfPlane.qExpansion 1 ⇑f ^ n

theorem qExpansion_injective {k : ℤ} (n : ℕ) [hn : NeZero n] (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k) : UpperHalfPlane.qExpansion ↑n ⇑f = 0 ↔ f = 0