The Function b

This file defines Viazovska's function b via its integral representations.

noncomputable def MagicFunction.b.ComplexIntegrands.Ψ₁' (r : ℝ) : ℂ → ℂ

Equations

• MagicFunction.b.ComplexIntegrands.Ψ₁' r z = ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def MagicFunction.b.ComplexIntegrands.Ψ₂' (r : ℝ) : ℂ → ℂ

Equations

• MagicFunction.b.ComplexIntegrands.Ψ₂' r z = ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def MagicFunction.b.ComplexIntegrands.Ψ₃' (r : ℝ) : ℂ → ℂ

Equations

• MagicFunction.b.ComplexIntegrands.Ψ₃' r z = ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def MagicFunction.b.ComplexIntegrands.Ψ₄' (r : ℝ) : ℂ → ℂ

Equations

• MagicFunction.b.ComplexIntegrands.Ψ₄' r z = ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def MagicFunction.b.ComplexIntegrands.Ψ₅' (r : ℝ) : ℂ → ℂ

Equations

• MagicFunction.b.ComplexIntegrands.Ψ₅' r z = ψI' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def MagicFunction.b.ComplexIntegrands.Ψ₆' (r : ℝ) : ℂ → ℂ

Equations

• MagicFunction.b.ComplexIntegrands.Ψ₆' r z = ψS' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

theorem MagicFunction.b.ComplexIntegrands.Ψ₁'_def (r : ℝ) : Ψ₁' r = fun (z : ℂ) => ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

theorem MagicFunction.b.ComplexIntegrands.Ψ₂'_def (r : ℝ) : Ψ₂' r = fun (z : ℂ) => ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

theorem MagicFunction.b.ComplexIntegrands.Ψ₃'_def (r : ℝ) : Ψ₃' r = fun (z : ℂ) => ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

theorem MagicFunction.b.ComplexIntegrands.Ψ₄'_def (r : ℝ) : Ψ₄' r = fun (z : ℂ) => ψT' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

theorem MagicFunction.b.ComplexIntegrands.Ψ₅'_def (r : ℝ) : Ψ₅' r = fun (z : ℂ) => ψI' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

theorem MagicFunction.b.ComplexIntegrands.Ψ₆'_def (r : ℝ) : Ψ₆' r = fun (z : ℂ) => ψS' z * Complex.exp (↑Real.pi * Complex.I * ↑r * z)

noncomputable def MagicFunction.b.RealIntegrands.Ψ₁ (r : ℝ) : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrands.Ψ₁ r t = Complex.I * MagicFunction.b.ComplexIntegrands.Ψ₁' r (MagicFunction.Parametrisations.z₁' t)

noncomputable def MagicFunction.b.RealIntegrands.Ψ₂ (r : ℝ) : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrands.Ψ₂ r t = MagicFunction.b.ComplexIntegrands.Ψ₂' r (MagicFunction.Parametrisations.z₂' t)

noncomputable def MagicFunction.b.RealIntegrands.Ψ₃ (r : ℝ) : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrands.Ψ₃ r t = Complex.I * MagicFunction.b.ComplexIntegrands.Ψ₃' r (MagicFunction.Parametrisations.z₃' t)

noncomputable def MagicFunction.b.RealIntegrands.Ψ₄ (r : ℝ) : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrands.Ψ₄ r t = -1 * MagicFunction.b.ComplexIntegrands.Ψ₄' r (MagicFunction.Parametrisations.z₄' t)

noncomputable def MagicFunction.b.RealIntegrands.Ψ₅ (r : ℝ) : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrands.Ψ₅ r t = Complex.I * MagicFunction.b.ComplexIntegrands.Ψ₅' r (MagicFunction.Parametrisations.z₅' t)

noncomputable def MagicFunction.b.RealIntegrands.Ψ₆ (r : ℝ) : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrands.Ψ₆ r t = Complex.I * MagicFunction.b.ComplexIntegrands.Ψ₆' r (MagicFunction.Parametrisations.z₆' t)

theorem MagicFunction.b.RealIntegrands.Ψ₁_def (r : ℝ) : Ψ₁ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Ψ₁' r (Parametrisations.z₁' t)

theorem MagicFunction.b.RealIntegrands.Ψ₂_def (r : ℝ) : Ψ₂ r = fun (t : ℝ) => ComplexIntegrands.Ψ₂' r (Parametrisations.z₂' t)

theorem MagicFunction.b.RealIntegrands.Ψ₃_def (r : ℝ) : Ψ₃ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Ψ₃' r (Parametrisations.z₃' t)

theorem MagicFunction.b.RealIntegrands.Ψ₄_def (r : ℝ) : Ψ₄ r = fun (t : ℝ) => -1 * ComplexIntegrands.Ψ₄' r (Parametrisations.z₄' t)

theorem MagicFunction.b.RealIntegrands.Ψ₅_def (r : ℝ) : Ψ₅ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Ψ₅' r (Parametrisations.z₅' t)

theorem MagicFunction.b.RealIntegrands.Ψ₆_def (r : ℝ) : Ψ₆ r = fun (t : ℝ) => Complex.I * ComplexIntegrands.Ψ₆' r (Parametrisations.z₆' t)

noncomputable def MagicFunction.b.RealIntegrals.J₁' : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrals.J₁' x = ∫ (t : ℝ) in 0..1, MagicFunction.b.RealIntegrands.Ψ₁ x t

noncomputable def MagicFunction.b.RealIntegrals.J₂' : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrals.J₂' x = ∫ (t : ℝ) in 0..1, MagicFunction.b.RealIntegrands.Ψ₂ x t

noncomputable def MagicFunction.b.RealIntegrals.J₃' : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrals.J₃' x = ∫ (t : ℝ) in 0..1, MagicFunction.b.RealIntegrands.Ψ₃ x t

noncomputable def MagicFunction.b.RealIntegrals.J₄' : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrals.J₄' x = ∫ (t : ℝ) in 0..1, MagicFunction.b.RealIntegrands.Ψ₄ x t

noncomputable def MagicFunction.b.RealIntegrals.J₅' : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrals.J₅' x = -2 * ∫ (t : ℝ) in 0..1, MagicFunction.b.RealIntegrands.Ψ₅ x t

noncomputable def MagicFunction.b.RealIntegrals.J₆' : ℝ → ℂ

Equations

• MagicFunction.b.RealIntegrals.J₆' x = 2 * ∫ (t : ℝ) in Set.Ici 1, MagicFunction.b.RealIntegrands.Ψ₆ x t

noncomputable def MagicFunction.b.RealIntegrals.b' : ℝ → ℂ

Equations

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

noncomputable def MagicFunction.b.RadialFunctions.J₁ : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

• MagicFunction.b.RadialFunctions.J₁ x = MagicFunction.b.RealIntegrals.J₁' (‖x‖ ^ 2)

noncomputable def MagicFunction.b.RadialFunctions.J₂ : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

• MagicFunction.b.RadialFunctions.J₂ x = MagicFunction.b.RealIntegrals.J₂' (‖x‖ ^ 2)

noncomputable def MagicFunction.b.RadialFunctions.J₃ : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

• MagicFunction.b.RadialFunctions.J₃ x = MagicFunction.b.RealIntegrals.J₃' (‖x‖ ^ 2)

noncomputable def MagicFunction.b.RadialFunctions.J₄ : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

• MagicFunction.b.RadialFunctions.J₄ x = MagicFunction.b.RealIntegrals.J₄' (‖x‖ ^ 2)

noncomputable def MagicFunction.b.RadialFunctions.J₅ : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

• MagicFunction.b.RadialFunctions.J₅ x = MagicFunction.b.RealIntegrals.J₅' (‖x‖ ^ 2)

noncomputable def MagicFunction.b.RadialFunctions.J₆ : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

• MagicFunction.b.RadialFunctions.J₆ x = MagicFunction.b.RealIntegrals.J₆' (‖x‖ ^ 2)

noncomputable def MagicFunction.b.RadialFunctions.b : EuclideanSpace ℝ (Fin 8) → ℂ

Equations

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

theorem MagicFunction.b.RadialFunctions.b_eq (x : EuclideanSpace ℝ (Fin 8)) : b x = J₁ x + J₂ x + J₃ x + J₄ x + J₅ x + J₆ x

theorem MagicFunction.b.RadialFunctions.J₁'_eq₀ (r : ℝ) : RealIntegrals.J₁' r = ∫ (t : ℝ) in 0..1, Complex.I * ψS' (-1 / (Parametrisations.z₁' t + 1)) * (Parametrisations.z₁' t + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * Parametrisations.z₁' t)

theorem MagicFunction.b.RadialFunctions.J₂'_eq₀ (r : ℝ) : RealIntegrals.J₂' r = ∫ (t : ℝ) in 0..1, ψS' (-1 / (Parametrisations.z₂' t + 1)) * (Parametrisations.z₂' t + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * Parametrisations.z₂' t)

theorem MagicFunction.b.RadialFunctions.J₃'_eq₀ (r : ℝ) : RealIntegrals.J₃' r = ∫ (t : ℝ) in 0..1, Complex.I * ψS' (-1 / (Parametrisations.z₃' t + 1)) * (Parametrisations.z₃' t + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * Parametrisations.z₃' t)

theorem MagicFunction.b.RadialFunctions.J₄'_eq₀ (r : ℝ) : RealIntegrals.J₄' r = ∫ (t : ℝ) in 0..1, -1 * ψS' (-1 / (Parametrisations.z₄' t + 1)) * (Parametrisations.z₄' t + 1) ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * Parametrisations.z₄' t)

theorem MagicFunction.b.RadialFunctions.J₅'_eq₀ (r : ℝ) : RealIntegrals.J₅' r = -2 * ∫ (t : ℝ) in 0..1, Complex.I * ψS' (-1 / Parametrisations.z₅' t) * Parametrisations.z₅' t ^ 2 * Complex.exp (↑Real.pi * Complex.I * ↑r * Parametrisations.z₅' t)

theorem MagicFunction.b.RadialFunctions.J₆'_eq₀ (r : ℝ) : RealIntegrals.J₆' r = 2 * ∫ (t : ℝ) in Set.Ici 1, Complex.I * ψS' (Parametrisations.z₆' t) * Complex.exp (↑Real.pi * Complex.I * ↑r * Parametrisations.z₆' t)