Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Topology on the upper half plane #

In this file we introduce a TopologicalSpace structure on the upper half plane and provide various instances.

source
instance UpperHalfPlane.instTopologicalSpace :
TopologicalSpace UpperHalfPlane
Equations
source
theorem UpperHalfPlane.isOpenEmbedding_coe :
Topology.IsOpenEmbedding UpperHalfPlane.coe
source
@[deprecated UpperHalfPlane.isOpenEmbedding_coe (since := "2024-10-18")]
theorem UpperHalfPlane.openEmbedding_coe :
Topology.IsOpenEmbedding UpperHalfPlane.coe

Alias of UpperHalfPlane.isOpenEmbedding_coe.

source
theorem UpperHalfPlane.isEmbedding_coe :
Topology.IsEmbedding UpperHalfPlane.coe
source
@[deprecated UpperHalfPlane.isEmbedding_coe (since := "2024-10-26")]
theorem UpperHalfPlane.embedding_coe :
Topology.IsEmbedding UpperHalfPlane.coe

Alias of UpperHalfPlane.isEmbedding_coe.

source
theorem UpperHalfPlane.continuous_coe :
Continuous UpperHalfPlane.coe
source
theorem UpperHalfPlane.continuous_re :
Continuous re
source
theorem UpperHalfPlane.continuous_im :
Continuous im
source
instance UpperHalfPlane.instSecondCountableTopology :
SecondCountableTopology UpperHalfPlane
source
instance UpperHalfPlane.instT3Space :
T3Space UpperHalfPlane
source
instance UpperHalfPlane.instT4Space :
T4Space UpperHalfPlane
source
instance UpperHalfPlane.instContractibleSpace :
ContractibleSpace UpperHalfPlane
source
instance UpperHalfPlane.instLocPathConnectedSpace :
LocPathConnectedSpace UpperHalfPlane
source
instance UpperHalfPlane.instNoncompactSpace :
NoncompactSpace UpperHalfPlane
source
instance UpperHalfPlane.instLocallyCompactSpace :
LocallyCompactSpace UpperHalfPlane
source
def UpperHalfPlane.verticalStrip (A B : ℝ) :
Set UpperHalfPlane

The vertical strip of width A and height B, defined by elements whose real part has absolute value less than or equal to A and imaginary part is at least B.

Equations
Instances For
    source
    theorem UpperHalfPlane.mem_verticalStrip_iff (A B : ℝ) (z : UpperHalfPlane) :
    z ∈ verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im
    source
    theorem UpperHalfPlane.verticalStrip_mono {A B A' B' : ℝ} (hA : A ≤ A') (hB : B' ≤ B) :
    verticalStrip A B ⊆ verticalStrip A' B'
    source
    theorem UpperHalfPlane.verticalStrip_mono_left {A A' : ℝ} (h : A ≤ A') (B : ℝ) :
    verticalStrip A B ⊆ verticalStrip A' B
    source
    theorem UpperHalfPlane.verticalStrip_anti_right (A : ℝ) {B B' : ℝ} (h : B' ≤ B) :
    verticalStrip A B ⊆ verticalStrip A B'
    source
    theorem UpperHalfPlane.subset_verticalStrip_of_isCompact {K : Set UpperHalfPlane} (hK : IsCompact K) :
    ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
    source
    theorem UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip (z : UpperHalfPlane) {N : ℕ} (hn : 0 < N) :
    ∃ (n : ℤ), ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
    source
    def UpperHalfPlane.ofComplex :
    PartialHomeomorph ℂ UpperHalfPlane

    A section ℂ → ℍ of the natural inclusion map, bundled as a PartialHomeomorph.

    Equations
    Instances For
      source
      def UpperHalfPlane.«term↑ₕ_» :
      Lean.ParserDescr

      Extend a function on ℍ arbitrarily to a function on all of ℂ.

      Equations
      Instances For
        source
        @[simp]
        theorem UpperHalfPlane.ofComplex_apply (z : UpperHalfPlane) :
        ↑ofComplex ↑z = z
        source
        theorem UpperHalfPlane.ofComplex_apply_eq_ite (w : ℂ) :
        ↑ofComplex w = if hw : 0 < w.im then ⟨w, hw⟩ else Classical.choice ⋯
        source
        theorem UpperHalfPlane.ofComplex_apply_of_im_pos {z : ℂ} (hz : 0 < z.im) :
        ↑ofComplex z = ⟨z, hz⟩
        source
        theorem UpperHalfPlane.ofComplex_apply_of_im_nonpos {w : ℂ} (hw : w.im ≤ 0) :
        ↑ofComplex w = Classical.choice ⋯
        source
        theorem UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos {w w' : ℂ} (hw : w.im ≤ 0) (hw' : w'.im ≤ 0) :
        ↑ofComplex w = ↑ofComplex w'
        source
        theorem UpperHalfPlane.comp_ofComplex (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) :
        (f ∘ ↑ofComplex) ↑z = f z
        source
        theorem UpperHalfPlane.comp_ofComplex_of_im_pos (f : UpperHalfPlane → ℂ) (z : ℂ) (hz : 0 < z.im) :
        (f ∘ ↑ofComplex) z = f ⟨z, hz⟩
        source
        theorem UpperHalfPlane.comp_ofComplex_of_im_le_zero (f : UpperHalfPlane → ℂ) (z z' : ℂ) (hz : z.im ≤ 0) (hz' : z'.im ≤ 0) :
        (f ∘ ↑ofComplex) z = (f ∘ ↑ofComplex) z'
        source
        theorem UpperHalfPlane.eventuallyEq_coe_comp_ofComplex {z : ℂ} (hz : 0 < z.im) :
        UpperHalfPlane.coe ∘ ↑ofComplex =ᶠ[nhds z] id