Manifold structure on the upper half plane.

In this file we define the complex manifold structure on the upper half-plane.

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 : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) 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) : MDifferentiableAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (↑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} : MDifferentiableAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) f τ ↔ DifferentiableAt ℂ (f ∘ ↑ofComplex) ↑τ

theorem UpperHalfPlane.mdifferentiable_iff {f : UpperHalfPlane → ℂ} : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) 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) ℝ) : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) fun (τ : UpperHalfPlane) => num g ↑τ

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

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

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

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

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

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

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

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