Exact grade expansion of a finite packet's momentum residual. The operators may be instantiated by the actual value/derivative jets at each space-time point; this file proves the finite algebra and does not assume an Euler solve.

noncomputable def EulerPacketResidual.residual {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 : ℕ) (κ : ℝ) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (p : ℕ → Q) : W

Residual, constructed using L.

Equations

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

def EulerPacketResidual.coefficient {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 : ℕ) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (p : ℕ → Q) (n : ℕ) : W

Coefficient, constructed using truncate.

Equations

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

theorem EulerPacketResidual.residual_eq_evaluate {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 : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (p : ℕ → Q) (hu : u 0 = 0) (hp : H (p 0) = 0) : residual M κ L G H B C u p = EulerFiniteGrades.evaluate (2 * M) κ (coefficient M L G H B C u p)

The fast terms lose one grade, with their potentially negative grade proved absent.

theorem EulerPacketResidual.residual_eq_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] (M K : ℕ) (hK : K ≤ 2 * M + 1) (κ : ℝ) (hκ : κ ≠ 0) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (p : ℕ → Q) (hu : u 0 = 0) (hp : H (p 0) = 0) (hcancel : ∀ n < K, coefficient M L G H B C u p n = 0) : residual M κ L G H B C u p = ∑ n ∈ Finset.Ico K (2 * M + 1), κ ^ n • coefficient M L G H B C u p n

Cancellation of each low coefficient removes precisely those grades from the actual residual.

theorem EulerPacketResidual.packet_residual_eq_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 : ℕ) (κ : ℝ) (hκ : κ ≠ 0) (L : V →ₗ[ℝ] W) (G H : Q →ₗ[ℝ] W) (B C : V →ₗ[ℝ] V →ₗ[ℝ] W) (u : ℕ → V) (p : ℕ → Q) (hu : u 0 = 0) (hp : H (p 0) = 0) (hcancel : ∀ n ≤ N, coefficient (N + 1) L G H B C u p n = 0) : residual (N + 1) κ L G H B C u p = ∑ n ∈ Finset.Ico (N + 1) (2 * N + 3), κ ^ n • coefficient (N + 1) L G H B C u p n

For N profiles plus the last divergence corrector, the remaining grades are N+1 through 2N+2.