Topology on the upper half plane

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

@[instance_reducible]

noncomputable instance UpperHalfPlane.instTopologicalSpace : TopologicalSpace UpperHalfPlane

Equations

• UpperHalfPlane.instTopologicalSpace = TopologicalSpace.induced UpperHalfPlane.coe inferInstance

theorem UpperHalfPlane.isEmbedding_coe : Topology.IsEmbedding UpperHalfPlane.coe

theorem UpperHalfPlane.isOpenEmbedding_coe : Topology.IsOpenEmbedding UpperHalfPlane.coe

theorem UpperHalfPlane.continuous_coe : Continuous UpperHalfPlane.coe

theorem UpperHalfPlane.continuous_re : Continuous re

theorem UpperHalfPlane.continuous_im : Continuous im

theorem Continuous.upperHalfPlaneMk {X : Type u_1} [TopologicalSpace X] {f : X → ℂ} (hf : Continuous f) (hf₀ : ∀ (x : X), 0 < (f x).im) : Continuous fun (x : X) => { coe := f x, coe_im_pos := ⋯ }

instance UpperHalfPlane.instSecondCountableTopology : SecondCountableTopology UpperHalfPlane

instance UpperHalfPlane.instT3Space : T3Space UpperHalfPlane

instance UpperHalfPlane.instT4Space : T4Space UpperHalfPlane

instance UpperHalfPlane.instContractibleSpace : ContractibleSpace UpperHalfPlane

instance UpperHalfPlane.instLocallyPathConnectedSpace : LocallyPathConnectedSpace UpperHalfPlane

instance UpperHalfPlane.instNoncompactSpace : NoncompactSpace UpperHalfPlane

instance UpperHalfPlane.instLocallyCompactSpace : LocallyCompactSpace UpperHalfPlane

instance UpperHalfPlane.instContinuousGLSMul : ContinuousConstSMul (GL (Fin 2) ℝ) UpperHalfPlane

Each element of GL(2, ℝ) defines a continuous map ℍ → ℍ.

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

• UpperHalfPlane.verticalStrip A B = {z : UpperHalfPlane | |z.re| ≤ A ∧ B ≤ z.im}

theorem UpperHalfPlane.mem_verticalStrip_iff (A B : ℝ) (z : UpperHalfPlane) : z ∈ verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im

theorem UpperHalfPlane.verticalStrip_mono {A B A' B' : ℝ} (hA : A ≤ A') (hB : B' ≤ B) : verticalStrip A B ⊆ verticalStrip A' B'

theorem UpperHalfPlane.verticalStrip_mono_left {A A' : ℝ} (h : A ≤ A') (B : ℝ) : verticalStrip A B ⊆ verticalStrip A' B

theorem UpperHalfPlane.verticalStrip_anti_right (A : ℝ) {B B' : ℝ} (h : B' ≤ B) : verticalStrip A B ⊆ verticalStrip A B'

theorem UpperHalfPlane.subset_verticalStrip_of_isCompact {K : Set UpperHalfPlane} (hK : IsCompact K) : ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B

theorem UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip (z : UpperHalfPlane) {N : ℕ} (hn : 0 < N) : ∃ (n : ℤ), ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im

noncomputable def UpperHalfPlane.ofComplex : OpenPartialHomeomorph ℂ UpperHalfPlane

A section ℂ → ℍ of the natural inclusion map, bundled as an OpenPartialHomeomorph.

Equations

• UpperHalfPlane.ofComplex = (Topology.IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe UpperHalfPlane.isOpenEmbedding_coe).symm

def UpperHalfPlane.«term↑ₕ_» : Lean.ParserDescr

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

Equations

• UpperHalfPlane.«term↑ₕ_» = Lean.ParserDescr.node `UpperHalfPlane.«term↑ₕ_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑ₕ") (Lean.ParserDescr.cat `term 0))

@[simp]

theorem UpperHalfPlane.ofComplex_apply (z : UpperHalfPlane) : ↑ofComplex ↑z = z

theorem UpperHalfPlane.ofComplex_apply_eq_ite (w : ℂ) : ↑ofComplex w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯

theorem UpperHalfPlane.ofComplex_apply_of_im_pos {z : ℂ} (hz : 0 < z.im) : ↑ofComplex z = { coe := z, coe_im_pos := hz }

theorem UpperHalfPlane.ofComplex_apply_of_im_nonpos {w : ℂ} (hw : w.im ≤ 0) : ↑ofComplex w = Classical.choice ⋯

theorem UpperHalfPlane.ofComplex_apply_eq_of_im_nonpos {w w' : ℂ} (hw : w.im ≤ 0) (hw' : w'.im ≤ 0) : ↑ofComplex w = ↑ofComplex w'

theorem UpperHalfPlane.comp_ofComplex (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : (f ∘ ↑ofComplex) ↑z = f z

theorem UpperHalfPlane.comp_ofComplex_of_im_pos (f : UpperHalfPlane → ℂ) (z : ℂ) (hz : 0 < z.im) : (f ∘ ↑ofComplex) z = f { coe := z, coe_im_pos := hz }

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'

theorem UpperHalfPlane.periodic_comp_ofComplex {f : UpperHalfPlane → ℂ} {h : ℝ} (hf : ∀ (τ : UpperHalfPlane), f (h +ᵥ τ) = f τ) : Function.Periodic (f ∘ ↑ofComplex) ↑h

theorem UpperHalfPlane.eventuallyEq_coe_comp_ofComplex {z : ℂ} (hz : 0 < z.im) : UpperHalfPlane.coe ∘ ↑ofComplex =ᶠ[nhds z] id

theorem UpperHalfPlane.continuousOn_ofComplex_I_mul : ContinuousOn (fun (t : ℝ) => ↑ofComplex (↑I * ↑t)) (Set.Ioi 0)

theorem UpperHalfPlane.J_smul (τ : UpperHalfPlane) : J • τ = ↑ofComplex (-(starRingEnd ℂ) ↑τ)

theorem UpperHalfPlane.isOpenMap_re : IsOpenMap re

theorem UpperHalfPlane.isOpenMap_im : IsOpenMap im

theorem UpperHalfPlane.isOpenMap_norm : IsOpenMap fun (τ : UpperHalfPlane) => ‖↑τ‖