SpherePacking.MagicFunction.a.Basic

source

noncomputable def MagicFunction.a.ComplexIntegrands.Φ₁' (r : ℝ) :

ℂ → ℂ

Equations

MagicFunction.a.ComplexIntegrands.Φ₁' r z = φ₀'' (-1 / (z + 1)) * (z + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

Instances For

source

noncomputable def MagicFunction.a.ComplexIntegrands.Φ₂' (r : ℝ) :

ℂ → ℂ

Equations

MagicFunction.a.ComplexIntegrands.Φ₂' r z = φ₀'' (-1 / (z + 1)) * (z + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

Instances For

source

noncomputable def MagicFunction.a.ComplexIntegrands.Φ₃' (r : ℝ) :

ℂ → ℂ

Equations

MagicFunction.a.ComplexIntegrands.Φ₃' r z = φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

Instances For

source

noncomputable def MagicFunction.a.ComplexIntegrands.Φ₄' (r : ℝ) :

ℂ → ℂ

Equations

MagicFunction.a.ComplexIntegrands.Φ₄' r z = φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

Instances For

source

noncomputable def MagicFunction.a.ComplexIntegrands.Φ₅' (r : ℝ) :

ℂ → ℂ

Equations

MagicFunction.a.ComplexIntegrands.Φ₅' r z = φ₀'' (-1 / z) * z ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

Instances For

source

noncomputable def MagicFunction.a.ComplexIntegrands.Φ₆' (r : ℝ) :

ℂ → ℂ

Equations

MagicFunction.a.ComplexIntegrands.Φ₆' r z = φ₀'' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

Instances For

source

theorem MagicFunction.a.ComplexIntegrands.Φ₁'_def (r : ℝ) :

Φ₁' r = fun (z : ℂ) => φ₀'' (-1 / (z + 1)) * (z + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

source

theorem MagicFunction.a.ComplexIntegrands.Φ₂'_def (r : ℝ) :

Φ₂' r = fun (z : ℂ) => φ₀'' (-1 / (z + 1)) * (z + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

source

theorem MagicFunction.a.ComplexIntegrands.Φ₃'_def (r : ℝ) :

Φ₃' r = fun (z : ℂ) => φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

source

theorem MagicFunction.a.ComplexIntegrands.Φ₄'_def (r : ℝ) :

Φ₄' r = fun (z : ℂ) => φ₀'' (-1 / (z - 1)) * (z - 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

source

theorem MagicFunction.a.ComplexIntegrands.Φ₅'_def (r : ℝ) :

Φ₅' r = fun (z : ℂ) => φ₀'' (-1 / z) * z ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

source

theorem MagicFunction.a.ComplexIntegrands.Φ₆'_def (r : ℝ) :

Φ₆' r = fun (z : ℂ) => φ₀'' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

source

noncomputable def MagicFunction.a.RealIntegrands.Φ₁ (r : ℝ) :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrands.Φ₁ r t = Complex.I * MagicFunction.a.ComplexIntegrands.Φ₁' r (MagicFunction.Parametrisations.z₁' t)

Instances For

source

noncomputable def MagicFunction.a.RealIntegrands.Φ₂ (r : ℝ) :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrands.Φ₂ r t = MagicFunction.a.ComplexIntegrands.Φ₂' r (MagicFunction.Parametrisations.z₂' t)

Instances For

source

noncomputable def MagicFunction.a.RealIntegrands.Φ₃ (r : ℝ) :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrands.Φ₃ r t = Complex.I * MagicFunction.a.ComplexIntegrands.Φ₃' r (MagicFunction.Parametrisations.z₃' t)

Instances For

source

noncomputable def MagicFunction.a.RealIntegrands.Φ₄ (r : ℝ) :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrands.Φ₄ r t = -1 * MagicFunction.a.ComplexIntegrands.Φ₄' r (MagicFunction.Parametrisations.z₄' t)

Instances For

source

noncomputable def MagicFunction.a.RealIntegrands.Φ₅ (r : ℝ) :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrands.Φ₅ r t = Complex.I * MagicFunction.a.ComplexIntegrands.Φ₅' r (MagicFunction.Parametrisations.z₅' t)

Instances For

source

noncomputable def MagicFunction.a.RealIntegrands.Φ₆ (r : ℝ) :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrands.Φ₆ r t = Complex.I * MagicFunction.a.ComplexIntegrands.Φ₆' r (MagicFunction.Parametrisations.z₆' t)

Instances For

source

theorem MagicFunction.a.RealIntegrands.Φ₁_def (r : ℝ) :

Φ₁ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Φ₁' r (Parametrisations.z₁' t)

source

theorem MagicFunction.a.RealIntegrands.Φ₂_def (r : ℝ) :

Φ₂ r = fun (t : ℝ) => ComplexIntegrands.Φ₂' r (Parametrisations.z₂' t)

source

theorem MagicFunction.a.RealIntegrands.Φ₃_def (r : ℝ) :

Φ₃ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Φ₃' r (Parametrisations.z₃' t)

source

theorem MagicFunction.a.RealIntegrands.Φ₄_def (r : ℝ) :

Φ₄ r = fun (t : ℝ) => -1 * ComplexIntegrands.Φ₄' r (Parametrisations.z₄' t)

source

theorem MagicFunction.a.RealIntegrands.Φ₅_def (r : ℝ) :

Φ₅ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Φ₅' r (Parametrisations.z₅' t)

source

theorem MagicFunction.a.RealIntegrands.Φ₆_def (r : ℝ) :

Φ₆ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Φ₆' r (Parametrisations.z₆' t)

source

noncomputable def MagicFunction.a.RealIntegrals.I₁' :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrals.I₁' x = ∫ (t : ℝ) in 0..1, MagicFunction.a.RealIntegrands.Φ₁ x t

Instances For

source

noncomputable def MagicFunction.a.RealIntegrals.I₂' :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrals.I₂' x = ∫ (t : ℝ) in 0..1, MagicFunction.a.RealIntegrands.Φ₂ x t

Instances For

source

noncomputable def MagicFunction.a.RealIntegrals.I₃' :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrals.I₃' x = ∫ (t : ℝ) in 0..1, MagicFunction.a.RealIntegrands.Φ₃ x t

Instances For

source

noncomputable def MagicFunction.a.RealIntegrals.I₄' :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrals.I₄' x = ∫ (t : ℝ) in 0..1, MagicFunction.a.RealIntegrands.Φ₄ x t

Instances For

source

noncomputable def MagicFunction.a.RealIntegrals.I₅' :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrals.I₅' x = -2 * ∫ (t : ℝ) in 0..1, MagicFunction.a.RealIntegrands.Φ₅ x t

Instances For

source

noncomputable def MagicFunction.a.RealIntegrals.I₆' :

ℝ → ℂ

Equations

MagicFunction.a.RealIntegrals.I₆' x = 2 * ∫ (t : ℝ) in Set.Ici 1, MagicFunction.a.RealIntegrands.Φ₆ x t

Instances For

source

noncomputable def MagicFunction.a.RealIntegrals.a' :

ℝ → ℂ

Equations

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

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.I₁ :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.I₁ x = MagicFunction.a.RealIntegrals.I₁' (‖x‖ ^ 2)

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.I₂ :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.I₂ x = MagicFunction.a.RealIntegrals.I₂' (‖x‖ ^ 2)

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.I₃ :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.I₃ x = MagicFunction.a.RealIntegrals.I₃' (‖x‖ ^ 2)

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.I₄ :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.I₄ x = MagicFunction.a.RealIntegrals.I₄' (‖x‖ ^ 2)

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.I₅ :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.I₅ x = MagicFunction.a.RealIntegrals.I₅' (‖x‖ ^ 2)

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.I₆ :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.I₆ x = MagicFunction.a.RealIntegrals.I₆' (‖x‖ ^ 2)

Instances For

source

noncomputable def MagicFunction.a.RadialFunctions.a :

EuclideanSpace ℝ (Fin 8) → ℂ

Equations

MagicFunction.a.RadialFunctions.a x = MagicFunction.a.RealIntegrals.a' (‖x‖ ^ 2)

Instances For

source

theorem MagicFunction.a.RadialFunctions.a_eq (x : EuclideanSpace ℝ (Fin 8)) :

a x = I₁ x + I₂ x + I₃ x + I₄ x + I₅ x + I₆ x

source

theorem MagicFunction.a.RadialFunctions.I₁_eq (x : EuclideanSpace ℝ (Fin 8)) :

I₁ x = RealIntegrals.I₁' (‖x‖ ^ 2)

source

theorem MagicFunction.a.RadialFunctions.I₂_eq (x : EuclideanSpace ℝ (Fin 8)) :

I₂ x = RealIntegrals.I₂' (‖x‖ ^ 2)

source

theorem MagicFunction.a.RadialFunctions.I₃_eq (x : EuclideanSpace ℝ (Fin 8)) :

I₃ x = RealIntegrals.I₃' (‖x‖ ^ 2)

source

theorem MagicFunction.a.RadialFunctions.I₄_eq (x : EuclideanSpace ℝ (Fin 8)) :

I₄ x = RealIntegrals.I₄' (‖x‖ ^ 2)

source

theorem MagicFunction.a.RadialFunctions.I₅_eq (x : EuclideanSpace ℝ (Fin 8)) :

I₅ x = RealIntegrals.I₅' (‖x‖ ^ 2)

source

theorem MagicFunction.a.RadialFunctions.I₆_eq (x : EuclideanSpace ℝ (Fin 8)) :

I₆ x = RealIntegrals.I₆' (‖x‖ ^ 2)

source

theorem MagicFunction.a.RadialFunctions.I₁'_eq (r : ℝ) :

RealIntegrals.I₁' r = ∫ (t : ℝ) in 0..1, -Complex.I * φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₁'_eq' (r : ℝ) :

RealIntegrals.I₁' r = -Complex.I * ∫ (t : ℝ) in 0..1, φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₁'_eq_Ioc (r : ℝ) :

RealIntegrals.I₁' r = ∫ (t : ℝ) in Set.Ioc 0 1, -Complex.I * φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₁'_eq'_Ioc (r : ℝ) :

RealIntegrals.I₁' r = -Complex.I * ∫ (t : ℝ) in 0..1, φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₂'_eq (r : ℝ) :

RealIntegrals.I₂' r = ∫ (t : ℝ) in 0..1, φ₀'' (-1 / (↑t + Complex.I)) * (↑t + Complex.I) ^ 2 * Complex.exp (-↑Real.pi * Complex.I * ↑r) * Complex.exp (↑Real.pi * Complex.I * ↑r * ↑t) * Complex.exp (-↑Real.pi * ↑r)

source

theorem MagicFunction.a.RadialFunctions.I₃'_eq (r : ℝ) :

RealIntegrals.I₃' r = ∫ (t : ℝ) in 0..1, -Complex.I * φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₃'_eq' (r : ℝ) :

RealIntegrals.I₃' r = -Complex.I * ∫ (t : ℝ) in 0..1, φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₃'_eq_Ioc (r : ℝ) :

RealIntegrals.I₃' r = ∫ (t : ℝ) in Set.Ioc 0 1, -Complex.I * φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₃'_eq'_Ioc (r : ℝ) :

RealIntegrals.I₃' r = -Complex.I * ∫ (t : ℝ) in Set.Ioc 0 1, φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₄'_eq (r : ℝ) :

RealIntegrals.I₄' r = ∫ (t : ℝ) in 0..1, -1 * φ₀'' (-1 / (-↑t + Complex.I)) * (-↑t + Complex.I) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r) * Complex.exp (-↑Real.pi * Complex.I * ↑r * ↑t) * Complex.exp (-↑Real.pi * ↑r)

source

theorem MagicFunction.a.RadialFunctions.I₅'_eq (r : ℝ) :

RealIntegrals.I₅' r = -2 * ∫ (t : ℝ) in 0..1, -Complex.I * φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₅'_eq' (r : ℝ) :

RealIntegrals.I₅' r = 2 * Complex.I * ∫ (t : ℝ) in 0..1, φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₅'_eq_Ioc (r : ℝ) :

RealIntegrals.I₅' r = -2 * ∫ (t : ℝ) in Set.Ioc 0 1, -Complex.I * φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₅'_eq'_Ioc (r : ℝ) :

RealIntegrals.I₅' r = 2 * Complex.I * ∫ (t : ℝ) in Set.Ioc 0 1, φ₀'' (-1 / (Complex.I * ↑t)) * ↑t ^ 2 * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₆'_eq (r : ℝ) :

RealIntegrals.I₆' r = 2 * ∫ (t : ℝ) in Set.Ici 1, Complex.I * φ₀'' (Complex.I * ↑t) * Complex.exp (-↑Real.pi * ↑r * ↑t)

source

theorem MagicFunction.a.RadialFunctions.I₆'_eq' (r : ℝ) :

RealIntegrals.I₆' r = 2 * Complex.I * ∫ (t : ℝ) in Set.Ici 1, φ₀'' (Complex.I * ↑t) * Complex.exp (-↑Real.pi * ↑r * ↑t)