Analyticity through ofComplex

Near τ, the chart of ℍ at τ reads a function f as its extension f ∘ ofComplex. A function holomorphic on the upper half-plane, extended to ℂ by ofComplex, is analytic at every point of the open upper half-plane. Holomorphy on ℍ is also invariant under the Möbius action of a positive-determinant real matrix, the biholomorphism UpperHalfPlane.mdifferentiable_smul exhibits. Polynomial functions of the coordinate, such as z ↦ P(z, 1) for a binary form P, are holomorphic.

Main declarations

• TauCeti.UpperHalfPlane.comp_chartAt_symm_eventuallyEq — near τ, a function read in the chart of ℍ at τ is its extension by ofComplex.
• TauCeti.UpperHalfPlane.analyticAt_comp_ofComplex.
• MvPolynomial.mdifferentiable_aeval_coe — z ↦ P(z, 1) is holomorphic for a polynomial P in two variables.
• TauCeti.UpperHalfPlane.mdifferentiable_comp_smul_iff — τ ↦ f (g • τ) is holomorphic exactly when f is, for g : GL (Fin 2) ℝ of positive determinant.
• TauCeti.UpperHalfPlane.not_accPt_zeros_comp_ofComplex and TauCeti.UpperHalfPlane.exists_isOpen_zeros_inter — a subset's zeros isolate in an open neighbourhood.

References

• AINTLIB LeanModularForms — the valence-formula development this file ports onto the current Mathlib pin.

theorem TauCeti.UpperHalfPlane.comp_chartAt_symm_eventuallyEq {α : Type u_1} (f : UpperHalfPlane → α) (τ : UpperHalfPlane) : f ∘ ↑(chartAt ℂ τ).symm =ᶠ[nhds ↑τ] f ∘ ↑UpperHalfPlane.ofComplex

The representative of f in the chart of ℍ at τ agrees with f ∘ ofComplex near τ.

theorem MvPolynomial.mdifferentiable_aeval_coe {R : Type u_1} [CommSemiring R] [Algebra R ℂ] (P : MvPolynomial (Fin 2) R) : MDiff fun (z : UpperHalfPlane) => (aeval ![↑z, 1]) P

For a polynomial P in two variables with coefficients mapping to ℂ, the function z ↦ P(z, 1) is holomorphic on ℍ.

theorem TauCeti.UpperHalfPlane.analyticAt_comp_ofComplex {f : UpperHalfPlane → ℂ} (hf : MDiff f) {w : ℂ} (hw : 0 < w.im) : AnalyticAt ℂ (f ∘ ↑UpperHalfPlane.ofComplex) w

A function holomorphic on ℍ composes with ofComplex to a function analytic at every point of the open upper half-plane.

theorem TauCeti.UpperHalfPlane.not_accPt_zeros_comp_ofComplex {g : UpperHalfPlane → ℂ} (hg : MDiff g) (hg0 : g ≠ 0) {x : ℂ} (hx : 0 < x.im) : ¬AccPt x (Filter.principal {z : ℂ | 0 < z.im ∧ (g ∘ ↑UpperHalfPlane.ofComplex) z = 0})

The zeros of a nonzero holomorphic function's complex extension do not accumulate at any point of the upper half-plane.

theorem TauCeti.UpperHalfPlane.exists_isOpen_zeros_inter {g : UpperHalfPlane → ℂ} (hg : MDiff g) (hg0 : g ≠ 0) {K : Set ℂ} (hK : K ⊆ {z : ℂ | 0 < z.im}) : ∃ (U : Set ℂ), IsOpen U ∧ K ⊆ U ∧ U ⊆ {z : ℂ | 0 < z.im} ∧ {z : ℂ | z ∈ U ∧ (g ∘ ↑UpperHalfPlane.ofComplex) z = 0} = {z : ℂ | z ∈ K ∧ (g ∘ ↑UpperHalfPlane.ofComplex) z = 0}

Any subset of the upper half-plane has an open neighbourhood in the upper half-plane containing no zeros of the function's complex extension beyond its own.

Holomorphy and the Möbius action

theorem TauCeti.UpperHalfPlane.mdifferentiable_comp_smul_iff {g : GL (Fin 2) ℝ} (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) {f : UpperHalfPlane → ℂ} : (MDiff fun (τ : UpperHalfPlane) => f (g • τ)) ↔ MDiff f

Holomorphy is invariant under a positive-determinant Möbius action. For any g : GL (Fin 2) ℝ with 0 < det g, the function τ ↦ f (g • τ) is holomorphic exactly when f is: g acts on ℍ by a biholomorphism, whose inverse is the action of g⁻¹, again of positive determinant.