Ratios of modular forms as Fricke fractions

A ratio of modular forms for a finite-index subgroup containing Γ(N) is locally a fraction of elements of ℂ[j, f_v]. The denominator is nonzero on a punctured neighbourhood of every point, so the statement applies at poles as well as regular points.

The normalization argument uses the holomorphic functions f g¹¹ Δ⁻ᵏ and g¹² Δ⁻ᵏ. Its auxiliary lemmas adapt the existing q-expansion bridge's toolkit; this file is a separate, handwritten extension and does not represent an additional Prove2Me node.

theorem ModularCurve.LevelN.exists_frickeFraction_of_modularForm (N : ℕ) [NeZero N] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] (hΓ : CongruenceSubgroup.Gamma N ≤ Γ) (k : ℤ) (f g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hg : g ≠ 0) : ∃ (a : UpperHalfPlane → ℂ) (b : UpperHalfPlane → ℂ), a ∈ ring N ∧ b ∈ ring N ∧ b ≠ 0 ∧ ∀ (τ : UpperHalfPlane), (∀ᶠ (z : ℂ) in nhdsWithin ↑τ {↑τ}ᶜ, b (↑UpperHalfPlane.ofComplex z) ≠ 0) ∧ (fun (z : ℂ) => f (↑UpperHalfPlane.ofComplex z) / g (↑UpperHalfPlane.ofComplex z)) =ᶠ[nhdsWithin ↑τ {↑τ}ᶜ] fun (z : ℂ) => a (↑UpperHalfPlane.ofComplex z) / b (↑UpperHalfPlane.ofComplex z)

A ratio of modular forms for a group containing Γ(N) is a rational expression in j and the Fricke functions, with equality on punctured neighbourhoods and nonzero denominator.