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

@[implicit_reducible]

instance UpperHalfPlane.instCoeOutComplex : CoeOut UpperHalfPlane ℂ

def UpperHalfPlane.I : UpperHalfPlane

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

@[implicit_reducible]

instance UpperHalfPlane.instInhabited : Inhabited UpperHalfPlane

@[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

def UpperHalfPlane.re (z : UpperHalfPlane) : ℝ

Real part

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

def Mathlib.Meta.Positivity.evalUpperHalfPlaneIm : PositivityExt

Extension for the positivity tactic: UpperHalfPlane.im.

def Mathlib.Meta.Positivity.evalUpperHalfPlaneCoe : PositivityExt

Extension for the positivity tactic: UpperHalfPlane.coe.

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

@[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

@[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.

theorem UpperHalfPlane.isOpen_upperHalfPlaneSet : IsOpen upperHalfPlaneSet

@[simp]

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