The upper half plane

This file defines UpperHalfPlane to be the upper half plane in ℂ.

We define the notation ℍ for the upper half plane available in the locale UpperHalfPlane so as not to conflict with the quaternions.

structure UpperHalfPlane : Type

The open upper half plane, denoted as ℍ within the UpperHalfPlane namespace

• coe : ℂ

  Canonical embedding of the upper half-plane into ℂ.

• coe_im_pos : 0 < (↑self).im

theorem UpperHalfPlane.ext_iff {x y : UpperHalfPlane} : x = y ↔ ↑x = ↑y

theorem UpperHalfPlane.ext {x y : UpperHalfPlane} (coe : ↑x = ↑y) : x = y

def UpperHalfPlane.termℍ : Lean.ParserDescr

The open upper half plane, denoted as ℍ within the UpperHalfPlane namespace

Equations

• UpperHalfPlane.termℍ = Lean.ParserDescr.node `UpperHalfPlane.termℍ 1024 (Lean.ParserDescr.symbol "ℍ")

@[implicit_reducible]

instance UpperHalfPlane.instCoeOutComplex : CoeOut UpperHalfPlane ℂ

Equations

• UpperHalfPlane.instCoeOutComplex = { coe := UpperHalfPlane.coe }

def UpperHalfPlane.I : UpperHalfPlane

Define I := √-1 as an element of the upper half plane.

Equations

• UpperHalfPlane.I = { coe := Complex.I, coe_im_pos := UpperHalfPlane.I._proof_1 }

noncomputable def UpperHalfPlane.ρ : UpperHalfPlane

Define the cube root of unity ρ := (-1 + √-3) / 2 as an element of the upper half plane.

Equations

• UpperHalfPlane.ρ = { coe := { re := -1 / 2, im := √3 / 2 }, coe_im_pos := UpperHalfPlane.ρ._proof_1 }

theorem UpperHalfPlane.ρ_sq : ↑ρ ^ 2 = -↑ρ - 1

theorem UpperHalfPlane.norm_ρ : ‖↑ρ‖ = 1

@[implicit_reducible]

instance UpperHalfPlane.instInhabited : Inhabited UpperHalfPlane

Equations

• UpperHalfPlane.instInhabited = { default := UpperHalfPlane.I }

@[simp]

theorem UpperHalfPlane.coe_inj {a b : UpperHalfPlane} : ↑a = ↑b ↔ a = b

@[deprecated UpperHalfPlane.coe_inj (since := "2026-01-31")]

theorem UpperHalfPlane.ext_iff' {a b : UpperHalfPlane} : ↑a = ↑b ↔ a = b

Alias of UpperHalfPlane.coe_inj.

theorem UpperHalfPlane.coe_injective : Function.Injective UpperHalfPlane.coe

instance UpperHalfPlane.canLift : CanLift ℂ UpperHalfPlane UpperHalfPlane.coe fun (z : ℂ) => 0 < z.im

theorem UpperHalfPlane.forall {P : UpperHalfPlane → Prop} : (∀ (z : UpperHalfPlane), P z) ↔ ∀ (z : ℂ) (hz : 0 < z.im), P { coe := z, coe_im_pos := hz }

theorem UpperHalfPlane.exists {P : UpperHalfPlane → Prop} : (∃ (z : UpperHalfPlane), P z) ↔ ∃ (z : ℂ) (hz : 0 < z.im), P { coe := z, coe_im_pos := hz }

def UpperHalfPlane.im (z : UpperHalfPlane) : ℝ

Imaginary part

Equations

• z.im = (↑z).im

def UpperHalfPlane.re (z : UpperHalfPlane) : ℝ

Real part

Equations

• z.re = (↑z).re

theorem UpperHalfPlane.ext_re_im {a b : UpperHalfPlane} (hre : a.re = b.re) (him : a.im = b.im) : a = b

Extensionality lemma in terms of UpperHalfPlane.re and UpperHalfPlane.im.

@[deprecated UpperHalfPlane.ext_re_im (since := "2026-01-29")]

theorem UpperHalfPlane.ext' {a b : UpperHalfPlane} (hre : a.re = b.re) (him : a.im = b.im) : a = b

Alias of UpperHalfPlane.ext_re_im.

---

Extensionality lemma in terms of UpperHalfPlane.re and UpperHalfPlane.im.

@[simp]

theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) : (↑z).im = z.im

@[simp]

theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) : (↑z).re = z.re

@[simp]

theorem UpperHalfPlane.mk_re (z : ℂ) (h : 0 < z.im) : { coe := z, coe_im_pos := h }.re = z.re

@[simp]

theorem UpperHalfPlane.mk_im (z : ℂ) (h : 0 < z.im) : { coe := z, coe_im_pos := h }.im = z.im

theorem UpperHalfPlane.coe_mk (z : ℂ) (h : 0 < z.im) : ↑{ coe := z, coe_im_pos := h } = z

@[simp]

theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : 0 < (↑z).im := ⋯) : { coe := ↑z, coe_im_pos := h } = z

@[simp]

theorem UpperHalfPlane.I_im : I.im = 1

@[simp]

theorem UpperHalfPlane.I_re : I.re = 0

@[simp]

theorem UpperHalfPlane.coe_I : ↑I = Complex.I

@[deprecated UpperHalfPlane.coe_mk (since := "2026-01-29")]

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

theorem UpperHalfPlane.re_add_im (z : UpperHalfPlane) : ↑z.re + ↑z.im * Complex.I = ↑z

theorem UpperHalfPlane.im_pos (z : UpperHalfPlane) : 0 < z.im

theorem UpperHalfPlane.im_ne_zero (z : UpperHalfPlane) : z.im ≠ 0

theorem UpperHalfPlane.ne_zero (z : UpperHalfPlane) : ↑z ≠ 0

theorem UpperHalfPlane.mem_slitPlane (z : UpperHalfPlane) : ↑z ∈ Complex.slitPlane

theorem UpperHalfPlane.eq_of_re_of_norm {τ τ' : UpperHalfPlane} (hre : τ.re = τ'.re) (hnorm : ‖↑τ‖ = ‖↑τ'‖) : τ = τ'

Criterion for equality in terms of real part and norm. Useful when working with the geometry of the fundamental domain.

def Mathlib.Meta.Positivity.evalUpperHalfPlaneIm : PositivityExt

Extension for the positivity tactic: UpperHalfPlane.im.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.Positivity.evalUpperHalfPlaneCoe : PositivityExt

Extension for the positivity tactic: UpperHalfPlane.coe.

Equations

• One or more equations did not get rendered due to their size.

theorem UpperHalfPlane.normSq_pos (z : UpperHalfPlane) : 0 < Complex.normSq ↑z

theorem UpperHalfPlane.normSq_ne_zero (z : UpperHalfPlane) : Complex.normSq ↑z ≠ 0

theorem UpperHalfPlane.im_inv_neg_coe_pos (z : UpperHalfPlane) : 0 < (-↑z)⁻¹.im

theorem UpperHalfPlane.im_pnat_div_pos (n : ℕ) [NeZero n] (z : UpperHalfPlane) : 0 < (-↑n / ↑z).im

theorem UpperHalfPlane.ne_ofReal (z : UpperHalfPlane) (x : ℝ) : ↑z ≠ ↑x

theorem UpperHalfPlane.ne_intCast (z : UpperHalfPlane) (n : ℤ) : ↑z ≠ ↑n

@[deprecated UpperHalfPlane.ne_intCast (since := "2026-01-29")]

theorem UpperHalfPlane.ne_int (z : UpperHalfPlane) (n : ℤ) : ↑z ≠ ↑n

Alias of UpperHalfPlane.ne_intCast.

theorem UpperHalfPlane.ne_natCast (z : UpperHalfPlane) (n : ℕ) : ↑z ≠ ↑n

@[deprecated UpperHalfPlane.ne_natCast (since := "2026-01-29")]

theorem UpperHalfPlane.ne_nat (z : UpperHalfPlane) (n : ℕ) : ↑z ≠ ↑n

Alias of UpperHalfPlane.ne_natCast.

@[implicit_reducible]

noncomputable instance UpperHalfPlane.posRealAction : MulAction { x : ℝ // 0 < x } UpperHalfPlane

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UpperHalfPlane.coe_pos_real_smul (x : { x : ℝ // 0 < x }) (z : UpperHalfPlane) : ↑(x • z) = ↑x • ↑z

@[simp]

theorem UpperHalfPlane.pos_real_im (x : { x : ℝ // 0 < x }) (z : UpperHalfPlane) : (x • z).im = ↑x * z.im

@[simp]

theorem UpperHalfPlane.pos_real_re (x : { x : ℝ // 0 < x }) (z : UpperHalfPlane) : (x • z).re = ↑x * z.re

theorem UpperHalfPlane.pos_real_smul_injective (z : UpperHalfPlane) : Function.Injective fun (x : { x : ℝ // 0 < x }) => x • z

@[implicit_reducible]

instance UpperHalfPlane.instAddActionReal : AddAction ℝ UpperHalfPlane

Equations

• UpperHalfPlane.instAddActionReal = { vadd := fun (x : ℝ) (z : UpperHalfPlane) => { coe := ↑x + ↑z, coe_im_pos := ⋯ }, add_vadd := ⋯, zero_vadd := ⋯ }

@[simp]

theorem UpperHalfPlane.coe_vadd (x : ℝ) (z : UpperHalfPlane) : ↑(x +ᵥ z) = ↑x + ↑z

@[simp]

theorem UpperHalfPlane.vadd_re (x : ℝ) (z : UpperHalfPlane) : (x +ᵥ z).re = x + z.re

@[simp]

theorem UpperHalfPlane.vadd_im (x : ℝ) (z : UpperHalfPlane) : (x +ᵥ z).im = z.im

@[simp]

theorem UpperHalfPlane.vadd_right_cancel_iff {x y : ℝ} (z : UpperHalfPlane) : x +ᵥ z = y +ᵥ z ↔ x = y

theorem UpperHalfPlane.vadd_left_injective (z : UpperHalfPlane) : Function.Injective fun (x : ℝ) => x +ᵥ z

instance UpperHalfPlane.instInfinite : Infinite UpperHalfPlane

instance UpperHalfPlane.instNontrivial : Nontrivial UpperHalfPlane

@[reducible, inline]

abbrev UpperHalfPlane.upperHalfPlaneSet : Set ℂ

The upper half plane as a subset of ℂ. This is convenient for taking derivatives of functions on the upper half plane.

Equations

• UpperHalfPlane.upperHalfPlaneSet = {z : ℂ | 0 < z.im}

theorem UpperHalfPlane.isOpen_upperHalfPlaneSet : IsOpen upperHalfPlaneSet

@[simp]

theorem UpperHalfPlane.range_coe : Set.range UpperHalfPlane.coe = upperHalfPlaneSet