Manifold structure on the upper half plane.

In this file we define the complex manifold structure on the upper half-plane, and show it is invariant under Moebius transformations. We also calculate the derivative, and give an explicit formula for its Jacobian determinant over ℝ (used in proving that the action preserves a suitable measure).

@[implicit_reducible]

noncomputable instance UpperHalfPlane.instChartedSpaceComplex : ChartedSpace ℂ UpperHalfPlane

Equations

• UpperHalfPlane.instChartedSpaceComplex = UpperHalfPlane.isOpenEmbedding_coe.singletonChartedSpace

instance UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat : IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ UpperHalfPlane

theorem UpperHalfPlane.contMDiff_coe {n : WithTop ℕ∞} : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n UpperHalfPlane.coe

The inclusion map ℍ → ℂ is a map of C^n manifolds.

theorem UpperHalfPlane.mdifferentiable_coe : MDiff UpperHalfPlane.coe

The inclusion map ℍ → ℂ is a differentiable map of manifolds.

theorem UpperHalfPlane.contMDiffAt_ofComplex {n : WithTop ℕ∞} {z : ℂ} (hz : 0 < z.im) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n (↑ofComplex) z

theorem UpperHalfPlane.mdifferentiableAt_ofComplex {z : ℂ} (hz : 0 < z.im) : MDiffAt ↑ofComplex z

theorem UpperHalfPlane.contMDiffAt_iff {n : WithTop ℕ∞} {f : UpperHalfPlane → ℂ} {τ : UpperHalfPlane} : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n f τ ↔ ContDiffAt ℂ n (f ∘ ↑ofComplex) ↑τ

theorem UpperHalfPlane.mdifferentiableAt_iff {f : UpperHalfPlane → ℂ} {τ : UpperHalfPlane} : MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ ↑ofComplex) ↑τ

theorem UpperHalfPlane.mdifferentiable_iff {f : UpperHalfPlane → ℂ} : MDiff f ↔ DifferentiableOn ℂ (f ∘ ↑ofComplex) {z : ℂ | 0 < z.im}

theorem UpperHalfPlane.contMDiff_num {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun (τ : UpperHalfPlane) => num g ↑τ

theorem UpperHalfPlane.contMDiff_denom {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun (τ : UpperHalfPlane) => denom g ↑τ

theorem UpperHalfPlane.contMDiff_denom_zpow {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ) (k : ℤ) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun (x : UpperHalfPlane) => denom g ↑x ^ k

theorem UpperHalfPlane.contMDiff_inv_denom {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun (τ : UpperHalfPlane) => (denom g ↑τ)⁻¹

theorem UpperHalfPlane.contMDiff_smul {n : WithTop ℕ∞} {g : GL (Fin 2) ℝ} (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun (τ : UpperHalfPlane) => g • τ

Each element of GL(2, ℝ)⁺ defines a map of C ^ n manifolds ℍ → ℍ.

theorem UpperHalfPlane.mdifferentiable_num (g : GL (Fin 2) ℝ) : MDiff fun (τ : UpperHalfPlane) => num g ↑τ

theorem UpperHalfPlane.mdifferentiable_denom (g : GL (Fin 2) ℝ) : MDiff fun (τ : UpperHalfPlane) => denom g ↑τ

theorem UpperHalfPlane.mdifferentiable_denom_zpow (g : GL (Fin 2) ℝ) (k : ℤ) : MDiff fun (x : UpperHalfPlane) => denom g ↑x ^ k

theorem UpperHalfPlane.mdifferentiable_inv_denom (g : GL (Fin 2) ℝ) : MDiff fun (τ : UpperHalfPlane) => (denom g ↑τ)⁻¹

theorem UpperHalfPlane.mdifferentiable_smul {g : GL (Fin 2) ℝ} (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) : MDiff fun (τ : UpperHalfPlane) => g • τ

Each element of GL(2, ℝ)⁺ defines a complex-differentiable map ℍ → ℍ.

theorem UpperHalfPlane.eq_zero_of_frequently {f : UpperHalfPlane → ℂ} (hf : MDiff f) {τ : UpperHalfPlane} (hτ : ∃ᶠ (z : UpperHalfPlane) in nhdsWithin τ {τ}ᶜ, f z = 0) : f = 0

theorem UpperHalfPlane.mul_eq_zero_iff {f g : UpperHalfPlane → ℂ} (hf : MDiff f) (hg : MDiff g) : f * g = 0 ↔ f = 0 ∨ g = 0

theorem UpperHalfPlane.prod_eq_zero_iff {ι : Type u_1} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι} (hf : ∀ i ∈ s, MDiff (f i)) : ∏ i ∈ s, f i = 0 ↔ ∃ i ∈ s, f i = 0

Explicit calculations of the derivative of τ ↦ g • τ

TODO: would it be better to reimplement these using mfderiv together with a trivialization of the tangent space of ℍ, rather than using ofComplex as we currently do? Or would that bring more pain than gain?

theorem UpperHalfPlane.hasStrictDerivAt_smul {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (τ : UpperHalfPlane) : HasStrictDerivAt (fun (z : ℂ) => ↑(g • ↑ofComplex z)) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ

theorem UpperHalfPlane.deriv_smul {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (τ : UpperHalfPlane) : deriv (fun (z : ℂ) => ↑(g • ↑ofComplex z)) ↑τ = ↑(↑g).det / denom g ↑τ ^ 2

theorem UpperHalfPlane.deriv_smul_ne_zero {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (τ : UpperHalfPlane) : deriv (fun (z : ℂ) => ↑(g • ↑ofComplex z)) ↑τ ≠ 0

theorem UpperHalfPlane.analyticAt_smul {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (τ : UpperHalfPlane) : AnalyticAt ℂ (fun (z : ℂ) => ↑(g • ↑ofComplex z)) ↑τ

theorem UpperHalfPlane.meromorphicOrderAt_comp_smul {f : UpperHalfPlane → ℂ} {τ : UpperHalfPlane} {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) : meromorphicOrderAt (fun (z : ℂ) => f (g • ↑ofComplex z)) ↑τ = meromorphicOrderAt (fun (z : ℂ) => f (↑ofComplex z)) ↑(g • τ)

noncomputable def UpperHalfPlane.smulFDeriv (g : GL (Fin 2) ℝ) (z : ℂ) : ℂ →L[ℝ] ℂ

ℝ-linear map from ℂ to itself, which we shall show is the real derivative of the GL(2, ℝ)-action on ℍ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UpperHalfPlane.smulFDeriv_J_mul (g : GL (Fin 2) ℝ) (z : ℂ) : smulFDeriv (J * g) z = -(↑Complex.conjCLE).comp (smulFDeriv g z)

theorem UpperHalfPlane.det_smulFDeriv (g : GL (Fin 2) ℝ) (z : ℂ) : (smulFDeriv g z).det = ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

Determinant of the derivative of g : ℍ → ℍ considered as an ℝ-linear map. This is used in the proof that the action is measure-preserving. Note this formula applies for both orientation- preserving and orientation-reserving isometries.

theorem UpperHalfPlane.hasStrictFDerivAt_smul (g : GL (Fin 2) ℝ) (τ : UpperHalfPlane) : HasStrictFDerivAt (fun (z : ℂ) => ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ