Act III: The Exact Formula for Navier-Stokes 3D

Binary-tree expansion and normal-form operators in Fourier variables. Zero sorry. Zero axiom. Zero variable.

inductive BinaryTree : Type

• leaf : BinaryTree
• node : BinaryTree → BinaryTree → BinaryTree

instance instDecidableEqBinaryTree : DecidableEq BinaryTree

Equations

• instDecidableEqBinaryTree = instDecidableEqBinaryTree.decEq

def instDecidableEqBinaryTree.decEq (x✝ x✝¹ : BinaryTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqBinaryTree.decEq BinaryTree.leaf BinaryTree.leaf = isTrue ⋯
• instDecidableEqBinaryTree.decEq BinaryTree.leaf (a.node a_1) = isFalse ⋯
• instDecidableEqBinaryTree.decEq (a.node a_1) BinaryTree.leaf = isFalse ⋯

def instInhabitedBinaryTree.default : BinaryTree

Equations

• instInhabitedBinaryTree.default = BinaryTree.leaf

instance instInhabitedBinaryTree : Inhabited BinaryTree

Equations

• instInhabitedBinaryTree = { default := instInhabitedBinaryTree.default }

def BinaryTree.size : BinaryTree → ℕ

Equations

• BinaryTree.leaf.size = 1
• (t1.node t2).size = t1.size + t2.size

def dotInt (p q : Index3) : ℤ

Equations

• dotInt p q = p 0 * q 0 + p 1 * q 1 + p 2 * q 2

def dotC (x y : Fin 3 → ℂ) : ℂ

Equations

• dotC x y = x 0 * y 0 + x 1 * y 1 + x 2 * y 2

def kC (k : Index3) : Fin 3 → ℂ

Equations

• kC k i = ↑(k i)

def lerayApply (k : Index3) (z : Fin 3 → ℂ) : Fin 3 → ℂ

Equations

• lerayApply k z = if hk : k = 0 then z else have kc := kC k; have kk := ↑(freqNormSq k); fun (j : Fin 3) => z j - kc j * dotC kc z / kk

def bilinearSymbol (k p q : Index3) (a b : Fin 3 → ℂ) (j : Fin 3) : ℂ

Equations

• bilinearSymbol k p q a b j = -Complex.I / 2 * lerayApply k (fun (i : Fin 3) => dotC a (kC q) * b i + dotC b (kC p) * a i) j

def isResonant (p q : Index3) : Prop

Equations

• isResonant p q = (dotInt p q = 0)

instance instDecidableIsResonant (p q : Index3) : Decidable (isResonant p q)

Equations

• instDecidableIsResonant p q = inferInstanceAs (Decidable (dotInt p q = 0))

def B_nr (k p q : Index3) (a b : Fin 3 → ℂ) (j : Fin 3) : ℂ

Equations

• B_nr k p q a b j = if isResonant p q then 0 else bilinearSymbol k p q a b j

def B_res (k p q : Index3) (a b : Fin 3 → ℂ) (j : Fin 3) : ℂ

Equations

• B_res k p q a b j = if isResonant p q then bilinearSymbol k p q a b j else 0

def laplacianSymbol (nu : ℝ) (k : Index3) : ℂ

Equations

• laplacianSymbol nu k = -↑nu * ↑(freqNormSq k)

def Qnr (nu : ℝ) (k p q : Index3) (a b : Fin 3 → ℂ) (j : Fin 3) : ℂ

Equations

• Qnr nu k p q a b j = if isResonant p q then 0 else have gap := laplacianSymbol nu k - laplacianSymbol nu p - laplacianSymbol nu q; 2 * bilinearSymbol k p q a b j / gap

def treeAlgebraicCoeff (t : BinaryTree) : (Fin t.size → Index3) → (Fin t.size → Fin 3 → ℂ) → Fin 3 → ℂ

Equations

• One or more equations did not get rendered due to their size.
• treeAlgebraicCoeff BinaryTree.leaf x_3 as = as ⟨0, Nat.zero_lt_one⟩

def treeTimeIntegral (nu : ℝ) (t : BinaryTree) : (Fin t.size → Index3) → ℝ → ℂ

Equations

• One or more equations did not get rendered due to their size.
• treeTimeIntegral nu BinaryTree.leaf ks x✝ = Complex.exp (-↑nu * ↑(freqNormSq (ks ⟨0, Nat.zero_lt_one⟩)) * ↑x✝)

theorem dotInt_ne_zero_of_not_resonant {p q : Index3} (h : ¬isResonant p q) : ↑(dotInt p q) ≠ 0

theorem dotInt_ne_zero_of_not_resonant_int {p q : Index3} (h : ¬isResonant p q) : dotInt p q ≠ 0

theorem laplacian_gap_eq (nu : ℝ) (p q : Index3) : laplacianSymbol nu (p + q) - laplacianSymbol nu p - laplacianSymbol nu q = -2 * ↑nu * ↑(dotInt p q)

theorem gap_exact_value (nu : ℝ) (p q : Index3) : laplacianSymbol nu (p + q) - laplacianSymbol nu p - laplacianSymbol nu q = -2 * ↑nu * ↑(dotInt p q)

theorem laplacian_gap_ne_zero_of_not_resonant (nu : ℝ) (hnu : nu ≠ 0) {p q : Index3} (h : ¬isResonant p q) : laplacianSymbol nu (p + q) - laplacianSymbol nu p - laplacianSymbol nu q ≠ 0

theorem gap_ne_zero_of_not_resonant (nu : ℝ) (hnu : nu ≠ 0) (p q : Index3) (hres : ¬isResonant p q) : laplacianSymbol nu (p + q) - laplacianSymbol nu p - laplacianSymbol nu q ≠ 0

theorem homological_equation (nu : ℝ) (hnu : nu ≠ 0) (k p q : Index3) (hk : k = p + q) (hgap : laplacianSymbol nu k - laplacianSymbol nu p - laplacianSymbol nu q ≠ 0) (a b : Fin 3 → ℂ) (j : Fin 3) : have Q := Qnr nu k p q a b j; have term1 := laplacianSymbol nu k * Q; have term2 := (laplacianSymbol nu p + laplacianSymbol nu q) * Q; term1 - term2 = 2 * B_nr k p q a b j

theorem homological_equation_unconditional (nu : ℝ) (hnu : nu ≠ 0) (k p q : Index3) (hk : k = p + q) (hres : ¬isResonant p q) (a b : Fin 3 → ℂ) (j : Fin 3) : have Q := Qnr nu k p q a b j; have term1 := laplacianSymbol nu k * Q; have term2 := (laplacianSymbol nu p + laplacianSymbol nu q) * Q; term1 - term2 = 2 * B_nr k p q a b j