Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Manifold structure on the upper half plane. #

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

source
๐Ÿ”ธ coverage
noncomputable instance UpperHalfPlane.instChartedSpaceComplex :
ChartedSpace โ„‚ UpperHalfPlane
Equations
    source
    ๐Ÿ“ coverage
    instance UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat :
    IsManifold (modelWithCornersSelf โ„‚ โ„‚) โŠค UpperHalfPlane
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiff_coe {n : WithTop โ„•โˆž} :
    ContMDiff (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n UpperHalfPlane.coe

    The inclusion map โ„ โ†’ โ„‚ is a map of C^n manifolds.

    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiable_coe :
    MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) UpperHalfPlane.coe

    The inclusion map โ„ โ†’ โ„‚ is a differentiable map of manifolds.

    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiffAt_ofComplex {n : WithTop โ„•โˆž} {z : โ„‚} (hz : 0 < z.im) :
    ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n (โ†‘ofComplex) z
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiableAt_ofComplex {z : โ„‚} (hz : 0 < z.im) :
    MDifferentiableAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) (โ†‘ofComplex) z
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiffAt_iff {n : WithTop โ„•โˆž} {f : UpperHalfPlane โ†’ โ„‚} {ฯ„ : UpperHalfPlane} :
    ContMDiffAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n f ฯ„ โ†” ContDiffAt โ„‚ n (f โˆ˜ โ†‘ofComplex) โ†‘ฯ„
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiableAt_iff {f : UpperHalfPlane โ†’ โ„‚} {ฯ„ : UpperHalfPlane} :
    MDifferentiableAt (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) f ฯ„ โ†” DifferentiableAt โ„‚ (f โˆ˜ โ†‘ofComplex) โ†‘ฯ„
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiable_iff {f : UpperHalfPlane โ†’ โ„‚} :
    MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) f โ†” DifferentiableOn โ„‚ (f โˆ˜ โ†‘ofComplex) {z : โ„‚ | 0 < z.im}
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiff_num {n : WithTop โ„•โˆž} (g : GL (Fin 2) โ„) :
    ContMDiff (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n fun (ฯ„ : UpperHalfPlane) => num g โ†‘ฯ„
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiff_denom {n : WithTop โ„•โˆž} (g : GL (Fin 2) โ„) :
    ContMDiff (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n fun (ฯ„ : UpperHalfPlane) => denom g โ†‘ฯ„
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiff_denom_zpow {n : WithTop โ„•โˆž} (g : GL (Fin 2) โ„) (k : โ„ค) :
    ContMDiff (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n fun (x : UpperHalfPlane) => denom g โ†‘x ^ k
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.contMDiff_inv_denom {n : WithTop โ„•โˆž} (g : GL (Fin 2) โ„) :
    ContMDiff (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) n fun (ฯ„ : UpperHalfPlane) => (denom g โ†‘ฯ„)โปยน
    source
    ๐Ÿ“ coverage
    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 โ„ โ†’ โ„.

    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiable_num (g : GL (Fin 2) โ„) :
    MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) fun (ฯ„ : UpperHalfPlane) => num g โ†‘ฯ„
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiable_denom (g : GL (Fin 2) โ„) :
    MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) fun (ฯ„ : UpperHalfPlane) => denom g โ†‘ฯ„
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiable_denom_zpow (g : GL (Fin 2) โ„) (k : โ„ค) :
    MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) fun (x : UpperHalfPlane) => denom g โ†‘x ^ k
    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.mdifferentiable_inv_denom (g : GL (Fin 2) โ„) :
    MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) fun (ฯ„ : UpperHalfPlane) => (denom g โ†‘ฯ„)โปยน
    source
    ๐Ÿ“ coverage
    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 โ„ โ†’ โ„.

    source
    ๐Ÿ“ coverage
    theorem UpperHalfPlane.eq_zero_of_frequently {f : UpperHalfPlane โ†’ โ„‚} (hf : MDifferentiable (modelWithCornersSelf โ„‚ โ„‚) (modelWithCornersSelf โ„‚ โ„‚) f) {ฯ„ : UpperHalfPlane} (hฯ„ : โˆƒแถ  (z : UpperHalfPlane) in nhdsWithin ฯ„ {ฯ„}แถœ, f z = 0) :
    f = 0
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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