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

theorem cuspFunction_mul_zero (n : ℕ) (a b : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma n) a) (g : ModularForm (CongruenceSubgroup.Gamma n) b) [inst : NeZero n] : SlashInvariantFormClass.cuspFunction n (f.mul g) 0 = SlashInvariantFormClass.cuspFunction n f 0 * SlashInvariantFormClass.cuspFunction n g 0

theorem qExpansion_mul_coeff_zero (n : ℕ) (a b : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma n) a) (g : ModularForm (CongruenceSubgroup.Gamma n) b) [NeZero n] : (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion n (f.mul g)) = (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion n f) * (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion n g)

theorem cuspFunction_mul (n : ℕ) (a b : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma n) a) (g : ModularForm (CongruenceSubgroup.Gamma n) b) [NeZero n] : SlashInvariantFormClass.cuspFunction n (f.mul g) = SlashInvariantFormClass.cuspFunction n f * SlashInvariantFormClass.cuspFunction n g

theorem derivWithin_mul2 (f g : ℂ → ℂ) (s : Set ℂ) (hf : DifferentiableOn ℂ f s) (hd : DifferentiableOn ℂ g s) : s.restrict (derivWithin (fun (y : ℂ) => f y * g y) s) = s.restrict (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 (CongruenceSubgroup.Gamma n) a) (g : ModularForm (CongruenceSubgroup.Gamma n) b) [NeZero n] : ModularFormClass.qExpansion n (f.mul g) = ModularFormClass.qExpansion n f * ModularFormClass.qExpansion n g

theorem cuspFunction_sub {k : ℤ} (n : ℕ) [NeZero n] (f g : ModularForm (CongruenceSubgroup.Gamma n) k) : SlashInvariantFormClass.cuspFunction n (f - g) = SlashInvariantFormClass.cuspFunction n f - SlashInvariantFormClass.cuspFunction n g

theorem iteratedDerivWithin_eq_iteratedDeriv {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜) (hs : UniqueDiffOn 𝕜 s) (h : ContDiffAt 𝕜 (↑n) f x) (hx : x ∈ s) : iteratedDerivWithin n f s x = iteratedDeriv n f x

theorem qExpansion_sub {k : ℤ} (f g : ModularForm (CongruenceSubgroup.Gamma 1) k) : ModularFormClass.qExpansion 1 (f - g) = ModularFormClass.qExpansion 1 f - ModularFormClass.qExpansion 1 g

theorem cuspFunction_add {k : ℤ} (n : ℕ) [NeZero n] (f g : ModularForm (CongruenceSubgroup.Gamma n) k) : SlashInvariantFormClass.cuspFunction n (f + g) = SlashInvariantFormClass.cuspFunction n f + SlashInvariantFormClass.cuspFunction n g

theorem qExpansion_add {k : ℤ} (f g : ModularForm (CongruenceSubgroup.Gamma 1) k) : ModularFormClass.qExpansion 1 (f + g) = ModularFormClass.qExpansion 1 f + ModularFormClass.qExpansion 1 g

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

theorem qExpansion_smul2 {k : ℤ} (n : ℕ) (a : ℂ) (f : ModularForm (CongruenceSubgroup.Gamma n) k) [NeZero n] : a • ModularFormClass.qExpansion n f = ModularFormClass.qExpansion n (a • f)

theorem qExpansion_smul {k : ℤ} (n : ℕ) (a : ℂ) (f : CuspForm (CongruenceSubgroup.Gamma n) k) [NeZero n] : a • ModularFormClass.qExpansion n f = ModularFormClass.qExpansion n (a • f)

instance instFunLikeForallUpperHalfPlaneComplex_spherePacking : FunLike (UpperHalfPlane → ℂ) UpperHalfPlane ℂ

Equations

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

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

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

theorem qExpansion_of_mul (a b : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma 1) a) (g : ModularForm (CongruenceSubgroup.Gamma 1) b) : ModularFormClass.qExpansion 1 (((DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) a) f * (DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) b) g) (a + b)) = ModularFormClass.qExpansion 1 f * ModularFormClass.qExpansion 1 g

@[simp]

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 (CongruenceSubgroup.Gamma 1) k) (n : ℕ) : ModularFormClass.qExpansion 1 (((DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) k) f ^ n) (↑n * k)) = ModularFormClass.qExpansion 1 f ^ n

theorem qExpansion_injective {k : ℤ} (n : ℕ) [NeZero n] (f : ModularForm (CongruenceSubgroup.Gamma n) k) : ModularFormClass.qExpansion n f = 0 ↔ f = 0

theorem qExpansion_zero {k : ℤ} (n : ℕ) [NeZero n] : ModularFormClass.qExpansion n 0 = 0