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

Equations

• UpperHalfPlane.instSmoothManifoldWithCornersComplexModelWithCornersSelf = ⋯

theorem UpperHalfPlane.smooth_coe : Smooth (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) UpperHalfPlane.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.smoothAt_ofComplex {z : ℂ} (hz : 0 < z.im) : SmoothAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (↑UpperHalfPlane.ofComplex) z

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}