Exact residual expansion with genuine derivatives within the prescribed time interval.

noncomputable def EulerPacketPointJets.slicedMomentumResidual (s : Set ℝ) (κ : ℝ) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : Domain → EulerSmoothLimit.Space) (p : Domain → ℝ) (z : Domain) : EulerSmoothLimit.Space

Sliced momentum residual, constructed using linearPart.

Equations

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

noncomputable def EulerPacketPointJets.slicedMomentumGrade (s : Set ℝ) (N : ℕ) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) (n : ℕ) : EulerSmoothLimit.Space

Sliced momentum grade, constructed using coefficient.

Equations

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

theorem EulerPacketPointJets.slicedMomentum_fieldSum_eq (s : Set ℝ) (N : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) (hs : UniqueDiffWithinAt ℝ s z.1) (hut : ∀ i ≤ N, DifferentiableWithinAt ℝ (fun (t : ℝ) => u i (t, z.2)) s z.1) (hux : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => u i (z.1, y)) z.2) (hpx : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p i (z.1, y)) z.2) (hu0 : slicedJet s (u 0) z = 0) (hp0 : (fastPressure m) (pressureJet (p 0) z) = 0) : slicedMomentumResidual s κ FInv M m (fieldSum N κ u) (fieldSum N κ p) z = EulerFiniteGrades.evaluate (2 * N) κ (slicedMomentumGrade s N FInv M m u p z)

theorem EulerPacketPointJets.slicedMomentum_fieldSum_tail (s : Set ℝ) (N : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) (hs : UniqueDiffWithinAt ℝ s z.1) (hut : ∀ i ≤ N + 1, DifferentiableWithinAt ℝ (fun (t : ℝ) => u i (t, z.2)) s z.1) (hux : ∀ i ≤ N + 1, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => u i (z.1, y)) z.2) (hpx : ∀ i ≤ N + 1, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p i (z.1, y)) z.2) (hu0 : slicedJet s (u 0) z = 0) (hp0 : (fastPressure m) (pressureJet (p 0) z) = 0) (hcancel : ∀ n ≤ N, slicedMomentumGrade s (N + 1) FInv M m u p z n = 0) : slicedMomentumResidual s κ FInv M m (fieldSum (N + 1) κ u) (fieldSum (N + 1) κ p) z = ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • slicedMomentumGrade s (N + 1) FInv M m u p z n

This identity is valid at both endpoints when s=[0,T] and T>0.