Low-order source guards can be carried from one actual physical Euler state to the next. The only update costs are the initial velocity gradient error and the proved upper pressure bound.

theorem EulerPacketPhysicalLowBounds.quadratic_lower_of_norm (M : Matrix) (e : ℝ) (he : ‖M‖ ≤ e) (z : EulerSmoothLimit.Space) : -e * ‖z‖ ^ 2 ≤ inner ℝ (M z) z

theorem EulerPacketPhysicalLowBounds.quadratic_lower_of_difference (M N : Matrix) (C e : ℝ) (hC : ∀ (z : EulerSmoothLimit.Space), -C * ‖z‖ ^ 2 ≤ inner ℝ (M z) z) (he : ‖N - M‖ ≤ e) (z : EulerSmoothLimit.Space) : -(C + e) * ‖z‖ ^ 2 ≤ inner ℝ (N z) z

theorem EulerParentPacketFrames.Evolution.initialStrain_eq {A : Parent} (E : Evolution A) (x : EulerSmoothLimit.Space) : A.initialStrain.field x = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) (A.ell • x)

theorem EulerParentPacketFrames.Evolution.initial_gradient_lower_exterior {A : Parent} (E : Evolution A) (H : LowBounds A) (x : EulerSmoothLimit.Space) (hx : H.r ≤ ‖x‖) (z : EulerSmoothLimit.Space) : -H.Be * ‖z‖ ^ 2 ≤ inner ℝ ((fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x) z) z

theorem EulerParentPacketFrames.Evolution.initial_gradient_lower_core {A : Parent} (E : Evolution A) (H : LowBounds A) (x : EulerSmoothLimit.Space) (hx : ‖x‖ < H.r) (z : EulerSmoothLimit.Space) : -H.Bc * ‖z‖ ^ 2 ≤ inner ℝ ((fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x) z) z

def EulerParentPacketFrames.Evolution.lowBoundsFromPhysical {A : Parent} (E : Evolution A) (Be Bc L r K : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrq : r ≤ 1 / 4) (hK : 0 ≤ K) (hexterior : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖x‖ → ∀ (z : EulerSmoothLimit.Space), -Be * ‖z‖ ^ 2 ≤ inner ℝ ((fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x) z) z) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖x‖ < r → ∀ (z : EulerSmoothLimit.Space), -Bc * ‖z‖ ^ 2 ≤ inner ℝ ((fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x) z) z) (hpressure : ∀ (t : ↑(Set.Icc 0 A.T)) (x z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (A.T ^ 2 / 2) + Be * A.T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * A.T ≤ 1 / 2) : LowBounds A

Low bounds from physical, constructed using A.lowBoundsOfPhysical.

Equations

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

noncomputable def EulerParentPacketFrames.Evolution.updateLowBounds {A : Parent} (E : Evolution A) {N : Parent} (F : Evolution N) (H : LowBounds A) (e K : ℝ) (he : 0 ≤ e) (hK : 0 ≤ K) (herror : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => F.velocity (0, y)) x - fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x‖ ≤ e) (hpressure : ∀ (t : ↑(Set.Icc 0 N.T)) (x z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (F.force t) x) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (N.T ^ 2 / 2) + (H.Be + e) * N.T + EulerMeanHarmonic.boundaryLocalizationC2 * (H.Bc + e) * H.r ^ 3 * N.T ≤ 1 / 2) : LowBounds N

Update low bounds, constructed using F.lowBoundsFromPhysical.

Equations

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