def Helicity.crossProduct (a b : Fin 3 → ℂ) : Fin 3 → ℂ

3D Cross Product for complex vectors.

Equations

• Helicity.crossProduct a b 0 = a 1 * b 2 - a 2 * b 1
• Helicity.crossProduct a b 1 = a 2 * b 0 - a 0 * b 2
• Helicity.crossProduct a b 2 = a 0 * b 1 - a 1 * b 0

def Helicity.fourierCoeffVector (u : ↥(MeasureTheory.Lp (EuclideanSpace ℝ (Fin 3)) 2 MeasureTheory.volume)) (k : Index3) : Fin 3 → ℂ

Fourier coefficients of a vector-valued L2 function.

Equations

• Helicity.fourierCoeffVector u k i = ∫ (x : Torus3), ↑((↑↑u x).ofLp i) * star ((torusMon k) x)

def Helicity.helicitySummand (k : Index3) (u_hat v_hat : Fin 3 → ℂ) : ℝ

The summand for the helicity bilinear form in Fourier space.

Equations

• Helicity.helicitySummand k u_hat v_hat = (∑ i : Fin 3, u_hat i * star (Complex.I • Helicity.crossProduct (fun (j : Fin 3) => ↑(k j)) v_hat i)).re

def Helicity.helicityBilinear (u v : ↥(MeasureTheory.Lp (EuclideanSpace ℝ (Fin 3)) 2 MeasureTheory.volume)) : ℝ

Continuous bilinear form associated with helicity.

Equations

• Helicity.helicityBilinear u v = ∑' (k : Index3), Helicity.helicitySummand k (Helicity.fourierCoeffVector u k) (Helicity.fourierCoeffVector v k)

def Helicity.helicity_functional (u : ↥(MeasureTheory.Lp (EuclideanSpace ℝ (Fin 3)) 2 MeasureTheory.volume)) : ℝ

The concrete helicity functional.

Equations

• Helicity.helicity_functional u = Helicity.helicityBilinear u u

Fourier-Space Beltrami Wave Construction

def Helicity.helicitySummandOf (k : Index3) (a : Fin 3 → ℂ) : ℝ

Equations

• Helicity.helicitySummandOf k a = Helicity.helicitySummand k a a

theorem Helicity.helicitySummand_at_e1 : helicitySummandOf Helicity.k_e1✝ Helicity.bA✝ = 2

theorem Helicity.helicitySummand_at_neg_e1 : helicitySummandOf (-Helicity.k_e1✝) Helicity.bA_conj✝ = 2

theorem Helicity.beltrami_fourier_helicity_ne_zero (k : Index3) (a : Fin 3 → ℂ) (h_ev : crossProduct (fun (i : Fin 3) => ↑(k i)) a = -Complex.I • a) (h_u : a ≠ 0) : helicitySummandOf k a ≠ 0

def Helicity.globalHelicity (u : ↥(MeasureTheory.Lp (EuclideanSpace ℝ (Fin 3)) 2 MeasureTheory.volume)) : ℝ

Equations

• Helicity.globalHelicity u = Helicity.helicity_functional u

def Helicity.beltramiCoefficient (u_val omega_val : Fin 3 → ℝ) : ℝ

Equations

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

theorem Helicity.sh_zero : helicity_functional 0 = 0

theorem Helicity.cauchy_schwarz_fin3 (a b : Fin 3 → ℂ) : ∑ i : Fin 3, (a i * star (b i)).re ≤ √(∑ i : Fin 3, Complex.normSq (a i)) * √(∑ i : Fin 3, Complex.normSq (b i))

theorem Helicity.cross_product_bound (k a : Fin 3 → ℂ) : ∑ i : Fin 3, Complex.normSq (crossProduct k a i) ≤ (∑ i : Fin 3, Complex.normSq (k i)) * ∑ i : Fin 3, Complex.normSq (a i)