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.

source

def UpperHalfPlane :

Type

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

Equations

UpperHalfPlane = { point : ℂ // 0 < point.im }

Instances For

source

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 "ℍ")

Instances For

source

def UpperHalfPlane.coe (z : UpperHalfPlane) :

ℂ

Canonical embedding of the upper half-plane into ℂ.

Equations

↑z = ↑z

Instances For

source

instance UpperHalfPlane.instCoeOutComplex :

CoeOut UpperHalfPlane ℂ

Equations

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

source

instance UpperHalfPlane.instInhabited :

Inhabited UpperHalfPlane

Equations

UpperHalfPlane.instInhabited = { default := ⟨Complex.I, UpperHalfPlane.instInhabited._proof_1 ⟩ }

source

theorem UpperHalfPlane.ext {a b : UpperHalfPlane} (h : ↑a = ↑b) :

a = b

source

theorem UpperHalfPlane.ext_iff {a b : UpperHalfPlane} :

a = b ↔ ↑a = ↑b

source

@[simp]

theorem UpperHalfPlane.ext_iff' {a b : UpperHalfPlane} :

↑a = ↑b ↔ a = b

source

instance UpperHalfPlane.canLift :

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

source

def UpperHalfPlane.im (z : UpperHalfPlane) :

ℝ

Imaginary part

Equations

z.im = (↑z).im

Instances For

source

def UpperHalfPlane.re (z : UpperHalfPlane) :

ℝ

Real part

Equations

z.re = (↑z).re

Instances For

source

theorem UpperHalfPlane.ext' {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.

source

def UpperHalfPlane.mk (z : ℂ) (h : 0 < z.im) :

UpperHalfPlane

Constructor for UpperHalfPlane. It is useful if ⟨z, h⟩ makes Lean use a wrong typeclass instance.

Equations

UpperHalfPlane.mk z h = ⟨z, h⟩

Instances For

source

@[simp]

theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) :

(↑z).im = z.im

source

@[simp]

theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) :

(↑z).re = z.re

source

@[simp]

theorem UpperHalfPlane.mk_re (z : ℂ) (h : 0 < z.im) :

(mk z h).re = z.re

source

@[simp]

theorem UpperHalfPlane.mk_im (z : ℂ) (h : 0 < z.im) :

(mk z h).im = z.im

source

@[simp]

theorem UpperHalfPlane.coe_mk (z : ℂ) (h : 0 < z.im) :

↑(mk z h) = z

source

@[simp]

theorem UpperHalfPlane.coe_mk_subtype {z : ℂ} (hz : 0 < z.im) :

↑⟨z, hz⟩ = z

source

instance UpperHalfPlane.instNontrivial :

Nontrivial UpperHalfPlane

source

@[simp]

theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : 0 < (↑z).im := ⋯) :

mk (↑z) h = z

source

theorem UpperHalfPlane.re_add_im (z : UpperHalfPlane) :

↑z.re + ↑z.im * Complex.I = ↑z

source

theorem UpperHalfPlane.im_pos (z : UpperHalfPlane) :

0 < z.im

source

theorem UpperHalfPlane.im_ne_zero (z : UpperHalfPlane) :

z.im ≠ 0

source

theorem UpperHalfPlane.ne_zero (z : UpperHalfPlane) :

↑z ≠ 0

source

def UpperHalfPlane.I :

UpperHalfPlane

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

Equations

UpperHalfPlane.I = ⟨Complex.I, UpperHalfPlane.instInhabited._proof_1 ⟩

Instances For

source

@[simp]

theorem UpperHalfPlane.I_im :

I.im = 1

source

@[simp]

theorem UpperHalfPlane.I_re :

I.re = 0

source

@[simp]

theorem UpperHalfPlane.coe_I :

↑I = Complex.I

source

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.

Instances For

source

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.

Instances For

source

theorem UpperHalfPlane.normSq_pos (z : UpperHalfPlane) :

0 < Complex.normSq ↑z

source

theorem UpperHalfPlane.normSq_ne_zero (z : UpperHalfPlane) :

Complex.normSq ↑z ≠ 0

source

theorem UpperHalfPlane.im_inv_neg_coe_pos (z : UpperHalfPlane) :

0 < (-↑z)⁻¹.im

source

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

↑z ≠ ↑n

source

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

↑z ≠ ↑n

source

instance UpperHalfPlane.posRealAction :

MulAction { x : ℝ // 0 < x } UpperHalfPlane

Equations

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

source

@[simp]

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

↑(x • z) = ↑x • ↑z

source

@[simp]

theorem UpperHalfPlane.pos_real_im (x : { x : ℝ // 0 < x }) (z : UpperHalfPlane) :

(x • z).im = ↑x * z.im

source

@[simp]

theorem UpperHalfPlane.pos_real_re (x : { x : ℝ // 0 < x }) (z : UpperHalfPlane) :

(x • z).re = ↑x * z.re

source

instance UpperHalfPlane.instAddActionReal :

AddAction ℝ UpperHalfPlane

Equations

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

source

@[simp]

theorem UpperHalfPlane.coe_vadd (x : ℝ) (z : UpperHalfPlane) :

↑(x +ᵥ z) = ↑x + ↑z

source

@[simp]

theorem UpperHalfPlane.vadd_re (x : ℝ) (z : UpperHalfPlane) :

(x +ᵥ z).re = x + z.re

source

@[simp]

theorem UpperHalfPlane.vadd_im (x : ℝ) (z : UpperHalfPlane) :

(x +ᵥ z).im = z.im

source

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

Instances For

source

theorem UpperHalfPlane.isOpen_upperHalfPlaneSet :

IsOpen upperHalfPlaneSet

Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

The upper half plane #