def MagicFunction.b.RealIntegrals.J₁' (x : ℝ) : ℂ

Equations

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

def MagicFunction.b.RealIntegrals.J₂' (x : ℝ) : ℂ

Equations

• MagicFunction.b.RealIntegrals.J₂' x = ∫ (t : ℝ) in 0..1, ψT' (MagicFunction.Parametrisations.z₁' t) * Complex.exp (↑Real.pi * Complex.I * ↑x * MagicFunction.Parametrisations.z₁' t)

def MagicFunction.b.RealIntegrals.J₃' (x : ℝ) : ℂ

Equations

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

def MagicFunction.b.RealIntegrals.J₄' (x : ℝ) : ℂ

Equations

• MagicFunction.b.RealIntegrals.J₄' x = ∫ (t : ℝ) in 0..1, ψT' (MagicFunction.Parametrisations.z₁' t) * Complex.exp (↑Real.pi * Complex.I * ↑x * MagicFunction.Parametrisations.z₄' t)

def MagicFunction.b.RealIntegrals.J₅' (x : ℝ) : ℂ

Equations

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

def MagicFunction.b.RealIntegrals.J₆' (x : ℝ) : ℂ

Equations

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

def MagicFunction.b.RealIntegrals.b' (x : ℝ) : ℂ

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def MagicFunction.b.RadialFunctions.a (x : EuclideanSpace ℝ (Fin 8)) : ℂ

Equations

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

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