Documentation

SpherePacking.MagicFunction.IntegralParametrisations

Integral Parametrisations #

Parametrisations of the contours used to define the magic-function integrals.

def MagicFunction.Parametrisations.z₁ (t : ↑(Set.Icc 0 1)) :

Equations

MagicFunction.Parametrisations.z₁ t = -1 + Complex.I * ↑↑t

Instances For

noncomputable def MagicFunction.Parametrisations.z₁' (t : ℝ) :

Equations

MagicFunction.Parametrisations.z₁' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₁ t

Instances For

def MagicFunction.Parametrisations.z₂ (t : ↑(Set.Icc 0 1)) :

Equations

MagicFunction.Parametrisations.z₂ t = -1 + ↑↑t + Complex.I

Instances For

noncomputable def MagicFunction.Parametrisations.z₂' (t : ℝ) :

Equations

MagicFunction.Parametrisations.z₂' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₂ t

Instances For

def MagicFunction.Parametrisations.z₃ (t : ↑(Set.Icc 0 1)) :

Equations

MagicFunction.Parametrisations.z₃ t = 1 + Complex.I * ↑↑t

Instances For

noncomputable def MagicFunction.Parametrisations.z₃' (t : ℝ) :

Equations

MagicFunction.Parametrisations.z₃' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₃ t

Instances For

def MagicFunction.Parametrisations.z₄ (t : ↑(Set.Icc 0 1)) :

Equations

MagicFunction.Parametrisations.z₄ t = 1 - ↑↑t + Complex.I

Instances For

noncomputable def MagicFunction.Parametrisations.z₄' (t : ℝ) :

Equations

MagicFunction.Parametrisations.z₄' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₄ t

Instances For

def MagicFunction.Parametrisations.z₅ (t : ↑(Set.Icc 0 1)) :

Equations

MagicFunction.Parametrisations.z₅ t = Complex.I * ↑↑t

Instances For

noncomputable def MagicFunction.Parametrisations.z₅' (t : ℝ) :

Equations

MagicFunction.Parametrisations.z₅' t = Set.IccExtend MagicFunction.Parametrisations.z₁'._proof_1 MagicFunction.Parametrisations.z₅ t

Instances For

def MagicFunction.Parametrisations.z₆ (t : ↑(Set.Ici 1)) :

Equations

MagicFunction.Parametrisations.z₆ t = Complex.I * ↑↑t

Instances For

noncomputable def MagicFunction.Parametrisations.z₆' (t : ℝ) :

Equations

MagicFunction.Parametrisations.z₆' t = Set.IciExtend MagicFunction.Parametrisations.z₆ t

Instances For

theorem MagicFunction.Parametrisations.im_z₁'_pos {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

0 < (z₁' t).im

theorem MagicFunction.Parametrisations.im_z₂'_pos {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

0 < (z₂' t).im

theorem MagicFunction.Parametrisations.im_z₃'_pos {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

0 < (z₃' t).im

theorem MagicFunction.Parametrisations.im_z₄'_pos {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

0 < (z₄' t).im

theorem MagicFunction.Parametrisations.im_z₅'_pos {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

0 < (z₅' t).im

theorem MagicFunction.Parametrisations.im_z₆'_pos {t : ℝ} (ht : t ∈ Set.Ici 1) :

0 < (z₆' t).im

theorem MagicFunction.Parametrisations.z₁'_mem_upperHalfPlane_set {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

z₁' t ∈ UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₂'_mem_upperHalfPlane_set {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₂' t ∈ UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₃'_mem_upperHalfPlane_set {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

z₃' t ∈ UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₄'_mem_upperHalfPlane_set {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₄' t ∈ UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₅'_mem_upperHalfPlane_set {t : ℝ} (ht : t ∈ Set.Ioc 0 1) :

z₅' t ∈ UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₆'_mem_upperHalfPlane_set {t : ℝ} (ht : t ∈ Set.Ici 1) :

z₆' t ∈ UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₁'_mapsto :

Set.MapsTo z₁' (Set.Ioc 0 1) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₂'_mapsto :

Set.MapsTo z₂' (Set.Icc 0 1) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₃'_mapsto :

Set.MapsTo z₃' (Set.Ioc 0 1) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₄'_mapsto :

Set.MapsTo z₄' (Set.Icc 0 1) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₅'_mapsto :

Set.MapsTo z₅' (Set.Ioc 0 1) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₆'_mapsto :

Set.MapsTo z₆' (Set.Ici 1) UpperHalfPlane.upperHalfPlaneSet

theorem MagicFunction.Parametrisations.z₁'_eq_z₁_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₁' t = z₁ ⟨t, ht⟩

theorem MagicFunction.Parametrisations.z₂'_eq_z₂_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₂' t = z₂ ⟨t, ht⟩

theorem MagicFunction.Parametrisations.z₃'_eq_z₃_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₃' t = z₃ ⟨t, ht⟩

theorem MagicFunction.Parametrisations.z₄'_eq_z₄_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₄' t = z₄ ⟨t, ht⟩

theorem MagicFunction.Parametrisations.z₅'_eq_z₅_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₅' t = z₅ ⟨t, ht⟩

theorem MagicFunction.Parametrisations.z₆'_eq_z₆_of_mem {t : ℝ} (ht : t ∈ Set.Ici 1) :

z₆' t = z₆ ⟨t, ht⟩

theorem MagicFunction.Parametrisations.z₁'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₁' t = -1 + Complex.I * ↑t

theorem MagicFunction.Parametrisations.z₂'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₂' t = -1 + ↑t + Complex.I

theorem MagicFunction.Parametrisations.z₃'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₃' t = 1 + Complex.I * ↑t

theorem MagicFunction.Parametrisations.z₄'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₄' t = 1 - ↑t + Complex.I

theorem MagicFunction.Parametrisations.z₅'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) :

z₅' t = Complex.I * ↑t

theorem MagicFunction.Parametrisations.z₆'_eq_of_mem {t : ℝ} (ht : t ∈ Set.Ici 1) :

z₆' t = Complex.I * ↑t

theorem MagicFunction.Parametrisations.neg_inv_one_add_eq_ST_coe (z : UpperHalfPlane) :

-1 / (↑z + 1) = ↑((ModularGroup.S * ModularGroup.T) • z)

theorem MagicFunction.Parametrisations.neg_inv_one_add_mem (z : UpperHalfPlane) :

0 < (-1 / (↑z + 1)).im

theorem MagicFunction.Parametrisations.neg_inv_one_add_eq_ST (z : UpperHalfPlane) :

{ coe := -1 / (↑z + 1), coe_im_pos := ⋯ } = (ModularGroup.S * ModularGroup.T) • z

theorem MagicFunction.Parametrisations.neg_inv_eq_S_coe (z : UpperHalfPlane) :

-1 / ↑z = ↑(ModularGroup.S • z)

theorem MagicFunction.Parametrisations.neg_inv_mem (z : UpperHalfPlane) :

0 < (-1 / ↑z).im

theorem MagicFunction.Parametrisations.neg_inv_eq_S (z : UpperHalfPlane) :

{ coe := -1 / ↑z, coe_im_pos := ⋯ } = ModularGroup.S • z

theorem MagicFunction.Parametrisations.neg_inv_mem_of_mem {w : ℂ} (hw : w ∈ UpperHalfPlane.upperHalfPlaneSet) :

-1 / w ∈ UpperHalfPlane.upperHalfPlaneSet

The Möbius map w ↦ -1/w sends the upper-half-plane set ℍ₀ ⊆ ℂ to itself. (Set-level analogue of neg_inv_mem, which is stated for the subtype ℍ.)

theorem MagicFunction.Parametrisations.neg_inv_mapsto :

Set.MapsTo (fun (w : ℂ) => -1 / w) UpperHalfPlane.upperHalfPlaneSet UpperHalfPlane.upperHalfPlaneSet

w ↦ -1/w maps ℍ₀ into ℍ₀.

theorem MagicFunction.Parametrisations.neg_inv_add_mapsto {c : ℂ} (hc : c.im = 0) :

Set.MapsTo (fun (z : ℂ) => -1 / (z + c)) UpperHalfPlane.upperHalfPlaneSet UpperHalfPlane.upperHalfPlaneSet

For a real shift c (c.im = 0), z ↦ -1/(z + c) maps ℍ₀ into ℍ₀.