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 an analytic map of manifolds.

@[deprecated UpperHalfPlane.contMDiff_coe (since := "2024-11-20")]

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

Alias of UpperHalfPlane.contMDiff_coe.

---

The inclusion map ℍ → ℂ is an analytic map of 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

@[deprecated UpperHalfPlane.contMDiffAt_ofComplex (since := "2024-11-20")]

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

Alias of UpperHalfPlane.contMDiffAt_ofComplex.

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

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}