Genuine cylinder-path witnesses for each of the fifteen known-force families.

noncomputable def EulerPacketCylinderField.PrefixFields.termField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (k : KnownTerm) (i j : ℕ) : Field P T (k.raw O p a i j)

Term field as an element of Field P T (k.raw O p a i j).

Equations

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

theorem EulerPacketCylinderField.KnownTerm.integral_zero_of_zeroMean {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (k : KnownTerm) (hk : k.zeroMean = true) (i j : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, k.raw O p a i j (↑t, x, θ) = 0

theorem EulerPacketCylinderField.KnownTerm.angleIndependent_of_meanOnly {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (k : KnownTerm) (hk : k.meanOnly = true) (i j : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : k.raw O p a i j (↑t, x, θ) = k.raw O p a i j (↑t, x, 0)

theorem EulerPacketCylinderField.angleMean_eq_of_angleIndependent {P : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (t : ℝ) (x : EulerSmoothLimit.Space) (h : ∀ (θ : ℝ), raw (t, x, θ) = raw (t, x, 0)) (θ : ℝ) : EulerPacketProfileRecursion.angleMean P raw (t, x, θ) = raw (t, x, θ)

noncomputable def EulerPacketCylinderField.KnownTerm.meanRaw (k : KnownTerm) (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (i j : ℕ) : EulerPacketProfileRecursion.VectorField

Mean raw, with branches according to k.zeroMean.

Equations

• k.meanRaw O p a i j = if k.zeroMean = true then 0 else EulerPacketProfileRecursion.angleMean O.period (k.raw O p a i j)

noncomputable def EulerPacketCylinderField.KnownTerm.highRaw (k : KnownTerm) (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (i j : ℕ) : EulerPacketProfileRecursion.VectorField

High raw, with branches according to k.meanOnly.

Equations

• k.highRaw O p a i j = if k.meanOnly = true then 0 else if k.zeroMean = true then k.raw O p a i j else k.raw O p a i j - EulerPacketProfileRecursion.angleMean O.period (k.raw O p a i j)

theorem EulerPacketCylinderField.KnownTerm.meanRaw_eq {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (k : KnownTerm) (i j : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : k.meanRaw O p a i j (↑t, x, θ) = EulerPacketProfileRecursion.angleMean O.period (k.raw O p a i j) (↑t, x, θ)

theorem EulerPacketCylinderField.KnownTerm.highRaw_eq {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hB : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (k : KnownTerm) (i j : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : k.highRaw O p a i j (↑t, x, θ) = k.raw O p a i j (↑t, x, θ) - EulerPacketProfileRecursion.angleMean O.period (k.raw O p a i j) (↑t, x, θ)

noncomputable def EulerPacketCylinderField.PrefixFields.meanTermField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (k : KnownTerm) (i j : ℕ) : Field P T (k.meanRaw O p a i j)

Mean term field as an element of Field P T (k.meanRaw O p a i j).

Equations

• F.meanTermField C hp hT Ct hCt pressure k i j = if h : k.zeroMean = true then (EulerPacketCylinderField.Field.zero P T).congr ⋯ else (F.termField C hp hT Ct hCt pressure k i j).angleMean.congr ⋯

noncomputable def EulerPacketCylinderField.PrefixFields.highTermField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (C : CoefficientData P T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (k : KnownTerm) (i j : ℕ) : Field P T (k.highRaw O p a i j)

High term field as an element of Field P T (k.highRaw O p a i j).

Equations

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