Actual continuous cylinder L² fields for every tail grade and for the finite tail sum.

Exact residual-tail grades. Fast pressure is absent beyond degree N, and only degree N+1 retains the linear terminal corrector and slow pressure.

theorem EulerFiniteGrades.shiftDown_convolution_eq {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (M n : ℕ) (B : V →ₗ[ℝ] V →ₗ[ℝ] W) (u v : ℕ → V) : shiftDown (2 * M) (convolution M B u v) n = convolution M B u v (n + 1)

theorem EulerPacketResidual.coefficient_assembled_tail {V : Type u_1} {Q : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup Q] [Module ℝ Q] [AddCommGroup W] [Module ℝ W] (N n : ℕ) (hn : N + 1 ≤ n) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u c : ℕ → V) (q π : ℕ → Q) : coefficient (N + 1) L G H B C (EulerFiniteGrades.assemble N u c) (EulerFiniteGrades.assemble N q π) n = (if n = N + 1 then L (c N) + G (π N) else 0) + EulerFiniteGrades.convolution (N + 1) B (EulerFiniteGrades.assemble N u c) (EulerFiniteGrades.assemble N u c) n + EulerFiniteGrades.convolution (N + 1) C (EulerFiniteGrades.assemble N u c) (EulerFiniteGrades.assemble N u c) (n + 1)

theorem EulerPacketProfileRecursion.assembledJets_eq_known (O : Operators) (N : ℕ) (a : ℕ → Profile) (ha : a 0 = 0) (z : EulerPacketPointJets.Domain) : assembledJets O N a z = knownJets O (N + 1) a z

The existing known-jet constructor is exactly the complete finite velocity family.

theorem EulerPacketProfileRecursion.recursiveGrade_tail (O : Operators) (N n : ℕ) (hn : N + 1 ≤ n) (a : ℕ → Profile) (ha : a 0 = 0) (z : EulerPacketPointJets.Domain) : recursiveGrade O N a z n = (if n = N + 1 then (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (a N).corrector z) + (EulerPacketPointJets.slowPressure (O.inverseFrame z)) (EulerPacketPointJets.pressureJet (a N).highPressure z) else 0) + EulerPacketPointJets.nonlinearGrade (N + 1) n (O.inverseFrame z) (O.normal z) (knownJets O (N + 1) a z)

noncomputable def EulerPacketCylinderField.PrefixFields.tailNonlinearField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T (N + 1) a) (C : CoefficientData P T O) (n : ℕ) : Field P T fun (z : EulerPacketPointJets.Domain) => EulerPacketPointJets.nonlinearGrade (N + 1) n (O.inverseFrame z) (O.normal z) (EulerPacketProfileRecursion.knownJets O (N + 1) a z)

Tail nonlinear field as an element of Field P T (fun z => nonlinearGrade (N+1) n (O.inverseFrame z) (O.normal z) (knownJets O (N+1) a z)).

Equations

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

noncomputable def EulerPacketCylinderField.PrefixFields.tailLinearField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T (N + 1) a) (C : CoefficientData P T O) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct) (pressure : Field P T (pressureGradient (a N).highPressure)) (n : ℕ) : Field P T fun (z : EulerPacketPointJets.Domain) => if n = N + 1 then (EulerPacketPointJets.linearPart (O.strain z)) (EulerPacketPointJets.slicedJet O.interval (a N).corrector z) + (EulerPacketPointJets.slowPressure (O.inverseFrame z)) (EulerPacketPointJets.pressureJet (a N).highPressure z) else 0

Tail linear field used in packet residual tail fields.

Equations

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

noncomputable def EulerPacketCylinderField.PrefixFields.tailGradeField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T (N + 1) a) (C : CoefficientData P T O) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct) (pressure : Field P T (pressureGradient (a N).highPressure)) (ha : a 0 = 0) (n : ℕ) (hn : N + 1 ≤ n) : Field P T fun (z : EulerPacketPointJets.Domain) => EulerPacketProfileRecursion.recursiveGrade O N a z n

Tail grade field as an element of Field P T (fun z => recursiveGrade O N a z n).

Equations

• F.tailGradeField C hT Ct hCt pressure ha n hn = ((F.tailLinearField C hT Ct hCt pressure n).add (F.tailNonlinearField C n)).congr ⋯

theorem EulerPacketCylinderField.PrefixFields.tailGradeField_path {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T (N + 1) a) (C : CoefficientData P T O) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct) (pressure : Field P T (pressureGradient (a N).highPressure)) (ha : a 0 = 0) (n : ℕ) (hn : N + 1 ≤ n) : (F.tailGradeField C hT Ct hCt pressure ha n hn).path = (F.tailLinearField C hT Ct hCt pressure n).path + (F.tailNonlinearField C n).path

def EulerPacketCylinderField.tailGrades (N : ℕ) : Finset ℕ

Tail grades, given by Ico (N+1) (2*N+3).

Equations

• EulerPacketCylinderField.tailGrades N = Finset.Ico (N + 1) (2 * N + 3)

theorem EulerPacketCylinderField.tailGrades_card (N : ℕ) : (tailGrades N).card = N + 2

noncomputable def EulerPacketCylinderField.PrefixFields.tailSumField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T (N + 1) a) (C : CoefficientData P T O) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct) (pressure : Field P T (pressureGradient (a N).highPressure)) (ha : a 0 = 0) (κ : ℝ) : Field P T fun (z : EulerPacketPointJets.Domain) => ∑ n ∈ tailGrades N, κ ^ n • EulerPacketProfileRecursion.recursiveGrade O N a z n

Tail sum field as an element of Field P T (fun z => ∑ n ∈ tailGrades N, κ^n • recursiveGrade O N a z n).

Equations

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

def EulerPacketCylinderField.ProfileRegularity.prefixThrough {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {S : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i)) : PrefixFields P T (N + 1) a

Prefix through, given by prefixFields (fun i hi => G i (by omega)).

Equations

• EulerPacketCylinderField.ProfileRegularity.prefixThrough hT G = EulerPacketCylinderField.ProfileRegularity.prefixFields fun (i : ℕ) (hi : i < N + 1) => G i ⋯

noncomputable def EulerPacketCylinderField.ProfileRegularity.tailGradeField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {S : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i)) (C : CoefficientData P T O) (ha : a 0 = 0) (n : ℕ) (hn : N + 1 ≤ n) : Field P T fun (z : EulerPacketPointJets.Domain) => EulerPacketProfileRecursion.recursiveGrade O N a z n

Tail grade field as an element of Field P T (fun z => recursiveGrade O N a z n).

Equations

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

noncomputable def EulerPacketCylinderField.ProfileRegularity.tailSumField {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {S : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ S (a i)) (C : CoefficientData P T O) (ha : a 0 = 0) (κ : ℝ) : Field P T fun (z : EulerPacketPointJets.Domain) => ∑ n ∈ tailGrades N, κ ^ n • EulerPacketProfileRecursion.recursiveGrade O N a z n

Tail sum field, given by (prefixThrough hT G).tailSumField C hT (G N le_rfl).correctorDerivative (G N le_rfl).corrector_time (G N le_rfl).pressure ha κ.

Equations

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