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.instSmoothManifoldWithCornersComplexModelWithCornersSelf : SmoothManifoldWithCorners (modelWithCornersSelf ℂ ℂ) UpperHalfPlane

theorem UpperHalfPlane.contMDiff_coe : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ UpperHalfPlane.coe

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

@[deprecated UpperHalfPlane.contMDiff_coe]

theorem UpperHalfPlane.smooth_coe : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ UpperHalfPlane.coe

Alias of UpperHalfPlane.contMDiff_coe.

---

The inclusion map ℍ → ℂ is a smooth 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 {z : ℂ} (hz : 0 < z.im) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑UpperHalfPlane.ofComplex) z

@[deprecated UpperHalfPlane.contMDiffAt_ofComplex]

theorem UpperHalfPlane.smoothAt_ofComplex {z : ℂ} (hz : 0 < z.im) : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (↑UpperHalfPlane.ofComplex) z

Alias of UpperHalfPlane.contMDiffAt_ofComplex.

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

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

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