Jacobi theta differentiability

This file contains the MDiff results for the Jacobi theta functions and the resulting modular form constructions H₂_MF, H₃_MF, and H₄_MF.

theorem H₂_SIF_MDifferentiable : MDiff ⇑H₂_SIF

theorem H₃_SIF_MDifferentiable : MDiff ⇑H₃_SIF

theorem H₄_SIF_MDifferentiable : MDiff ⇑H₄_SIF

theorem H₂_MDifferentiable : MDiff H₂

theorem H₃_MDifferentiable : MDiff H₃

theorem H₄_MDifferentiable : MDiff H₄

theorem differentiableAt_jacobiTheta₂_half (τ : UpperHalfPlane) : DifferentiableAt ℂ (fun (t : ℂ) => jacobiTheta₂ (t / 2) t) ↑τ

Differentiability of t ↦ jacobiTheta₂(t/2, t) at points in the upper half-plane.

theorem Θ₂_MDifferentiable : MDiff Θ₂

noncomputable def H₂_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₂_MF = { toSlashInvariantForm := H₂_SIF, holo' := H₂_SIF_MDifferentiable, bdd_at_cusps' := @H₂_MF._proof_1 }

noncomputable def H₃_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₃_MF = { toSlashInvariantForm := H₃_SIF, holo' := H₃_SIF_MDifferentiable, bdd_at_cusps' := @H₃_MF._proof_1 }

noncomputable def H₄_MF : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 2)) 2

Equations

• H₄_MF = { toSlashInvariantForm := H₄_SIF, holo' := H₄_SIF_MDifferentiable, bdd_at_cusps' := @H₄_MF._proof_1 }

@[simp]

theorem H₂_MF_coe : ⇑H₂_MF = H₂

@[simp]

theorem H₃_MF_coe : ⇑H₃_MF = H₃

@[simp]

theorem H₄_MF_coe : ⇑H₄_MF = H₄