Research proof index

Use jacobiTheta₂_functional_equation

These three transformation laws follow directly from tsum definition.

H₄(it) > 0 for all t > 0. Blueprint: Corollary 6.43 - H₄ is positive on the imaginary axis. Proof strategy: Use the modular S-transformation relating H₄ and H₂. From H₄_S_action: (H₄ ∣[2] S) = -H₂ From ResToImagAxis.SlashActionS: relates values at t and 1/t. This gives H₂(i/t) = t² * H₄(it), so H₄(it) > 0 follows from H₂(i/t) > 0.

Bounded denominators: if b is any finite K-basis of L and ϖ is a uniformiser of K, then a large enough power of ϖ multiplies every integer of L into the 𝒪[K]-lattice spanned by b. This is the key analytic input both for Module.Finite 𝒪[K] 𝒪[L] (see below) and, applied to a normal basis, for the construction of an open cohomologi...

Every element of L is carried into the integers 𝒪[L] by a large enough power of a uniformiser of K.

H₂, H₃, H₄ are modular forms of weight 2 and level Γ(2) -/ noncomputable def H₂_SIF : SlashInvariantForm (Γ 2) 2 where toFun := H₂ slash_action_eq' := slashaction_generators_Γ2 H₂ (2 : ℤ) H₂_α_action H₂_β_action H₂_negI_action noncomputable def H₃_SIF : SlashInvariantForm (Γ 2) 2 where toFun := H₃ slash_action_eq' := slashaction_generators_Γ2 H₃ (2 : ℤ) H...