Manifold structure on the upper half plane. #
In this file we define the complex manifold structure on the upper half-plane.
The inclusion map ℍ → ℂ
is a map of C^n
manifolds.
@[deprecated UpperHalfPlane.contMDiff_coe (since := "2024-11-20")]
Alias of UpperHalfPlane.contMDiff_coe
.
The inclusion map ℍ → ℂ
is a map of C^n
manifolds.
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.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 ℍ → ℍ
.