Actual path and time-derivative witnesses for finite coefficient assembly.

noncomputable def EulerPacketCylinderField.Field.truncateFamily {P T : ℝ} [Fact (0 < P)] (M : ℕ) (f : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → i ≤ M → Field P T (f i)) (n : ℕ) : Field P T (EulerFiniteGrades.truncate M f n)

Truncate family as an element of Field P T (truncate M f n).

Equations

• EulerPacketCylinderField.Field.truncateFamily M f G n = if hn : n ≤ M then (G n hn).congr ⋯ else (EulerPacketCylinderField.Field.zero P T).congr ⋯

noncomputable def EulerPacketCylinderField.Field.assembleFamily {P T : ℝ} [Fact (0 < P)] (M : ℕ) (f c : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → i ≤ M → Field P T (f i)) (H : (i : ℕ) → i ≤ M → Field P T (c i)) (n : ℕ) : Field P T (EulerFiniteGrades.assemble M f c n)

Assemble family used in packet finite field algebra.

Equations

• EulerPacketCylinderField.Field.assembleFamily M f c G H 0 = (EulerPacketCylinderField.Field.truncateFamily M f G 0).congr ⋯
• EulerPacketCylinderField.Field.assembleFamily M f c G H n.succ = (EulerPacketCylinderField.Field.truncateFamily M f G (n + 1)).add (EulerPacketCylinderField.Field.truncateFamily M c H n)

noncomputable def EulerPacketCylinderField.Field.evaluateFamily {P T : ℝ} [Fact (0 < P)] (M : ℕ) (κ : ℝ) (f : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → Field P T (f i)) : Field P T (EulerPacketPointJets.fieldSum M κ f)

Evaluate family as an element of Field P T (fieldSum M κ f).

Equations

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

theorem EulerPacketCylinderField.TimeDerivative.truncateFamily {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} (M : ℕ) (f f' : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → i ≤ M → Field P T (f i)) (G' : (i : ℕ) → i ≤ M → Field P T (f' i)) (hG : ∀ (i : ℕ) (hi : i ≤ M), TimeDerivative hT (G i hi) (G' i hi)) (n : ℕ) : TimeDerivative hT (Field.truncateFamily M f G n) (Field.truncateFamily M f' G' n)

theorem EulerPacketCylinderField.TimeDerivative.assembleFamily {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} (M : ℕ) (f f' c c' : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → i ≤ M → Field P T (f i)) (G' : (i : ℕ) → i ≤ M → Field P T (f' i)) (H : (i : ℕ) → i ≤ M → Field P T (c i)) (H' : (i : ℕ) → i ≤ M → Field P T (c' i)) (hG : ∀ (i : ℕ) (hi : i ≤ M), TimeDerivative hT (G i hi) (G' i hi)) (hH : ∀ (i : ℕ) (hi : i ≤ M), TimeDerivative hT (H i hi) (H' i hi)) (n : ℕ) : TimeDerivative hT (Field.assembleFamily M f c G H n) (Field.assembleFamily M f' c' G' H' n)

theorem EulerPacketCylinderField.TimeDerivative.evaluateFamily {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} (M : ℕ) (κ : ℝ) (f f' : ℕ → EulerPacketProfileRecursion.VectorField) (G : (i : ℕ) → Field P T (f i)) (G' : (i : ℕ) → Field P T (f' i)) (hG : ∀ (i : ℕ), TimeDerivative hT (G i) (G' i)) : TimeDerivative hT (Field.evaluateFamily M κ f G) (Field.evaluateFamily M κ f' G')