The low coefficients of the actual packet residual, before solving their equations.

The graded expansion and tail estimate for the actual normalized momentum expression.

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

Momentum grade, constructed using coefficient.

Equations

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

theorem EulerPacketPointJets.momentum_fieldSum_eq (N : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (u i) z) (hp : ∀ i ≤ N, DifferentiableAt ℝ (p i) z) (hu0 : jet (u 0) z = 0) (hp0 : (fastPressure m) (jet (p 0) z) = 0) : momentumResidual κ FInv M m (fieldSum N κ u) (fieldSum N κ p) z = EulerFiniteGrades.evaluate (2 * N) κ (momentumGrade N FInv M m u p z)

The equality expands the actual derivatives of the finite velocity and pressure sums.

theorem EulerPacketPointJets.momentum_fieldSum_tail (N : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) (hu : ∀ i ≤ N + 1, DifferentiableAt ℝ (u i) z) (hp : ∀ i ≤ N + 1, DifferentiableAt ℝ (p i) z) (hu0 : jet (u 0) z = 0) (hp0 : (fastPressure m) (jet (p 0) z) = 0) (hcancel : ∀ n ≤ N, momentumGrade (N + 1) FInv M m u p z n = 0) : momentumResidual κ FInv M m (fieldSum (N + 1) κ u) (fieldSum (N + 1) κ p) z = ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • momentumGrade (N + 1) FInv M m u p z n

The source's finite packet has no residual grades through N once its coefficient equations hold.

theorem EulerPacketPointJets.norm_momentum_fieldSum_le (N : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) (hu : ∀ i ≤ N + 1, DifferentiableAt ℝ (u i) z) (hp : ∀ i ≤ N + 1, DifferentiableAt ℝ (p i) z) (hu0 : jet (u 0) z = 0) (hp0 : (fastPressure m) (jet (p 0) z) = 0) (hcancel : ∀ n ≤ N, momentumGrade (N + 1) FInv M m u p z n = 0) : ‖momentumResidual κ FInv M m (fieldSum (N + 1) κ u) (fieldSum (N + 1) κ p) z‖ ≤ ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), |κ| ^ n * ‖momentumGrade (N + 1) FInv M m u p z n‖

A bound on the actual residual follows from the surviving coefficient norms.

theorem EulerPacketResidual.coefficient_eq_diagonal {V : Type u_1} {Q : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup Q] [Module ℝ Q] [AddCommGroup W] [Module ℝ W] (M n : ℕ) (hn : n + 1 ≤ M) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (p : ℕ → Q) : coefficient M L G H B C u p n = L (u n) + G (p n) + H (p (n + 1)) + ∑ i ∈ Finset.range (n + 1), (B (u i)) (u (n - i)) + ∑ i ∈ Finset.range (n + 2), (C (u i)) (u (n + 1 - i))

theorem EulerPacketPointJets.momentumGrade_eq_diagonal (N n : ℕ) (hn : n + 1 ≤ N) (FInv M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m : EulerSmoothLimit.Space) (u : ℕ → Domain → EulerSmoothLimit.Space) (p : ℕ → Domain → ℝ) (z : Domain) : momentumGrade N FInv M m u p z n = (linearPart M) (jet (u n) z) + (slowPressure FInv) (jet (p n) z) + (fastPressure m) (jet (p (n + 1)) z) + ∑ i ∈ Finset.range (n + 1), ((slowAdvection FInv) (jet (u i) z)) (jet (u (n - i)) z) + ∑ i ∈ Finset.range (n + 2), ((fastAdvection m) (jet (u i) z)) (jet (u (n + 1 - i)) z)

This is the coefficient equation used in the source recursion, with actual derivatives.