The low-order estimates behind source (20). The upper quadratic-form bound uses only the negative part of the angular derivative. Its cost therefore retains the narrow-profile factor which is absent from the absolute Hessian bound.

@[reducible, inline]

abbrev EulerPacketPhysicalLowBounds.Matrix : Type

Matrix: an abbreviation for Space →L[ℝ] Space.

Equations

• EulerPacketPhysicalLowBounds.Matrix = (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

noncomputable def EulerPacketPhysicalLowBounds.shearTerm (amp slope : ℝ) (r w : EulerSmoothLimit.Space) : Matrix

Shear term, given by (amp*slope) • rankOne ℝ w r.

Equations

• EulerPacketPhysicalLowBounds.shearTerm amp slope r w = (amp * slope) • ((InnerProductSpace.rankOne ℝ) w) r

noncomputable def EulerPacketPhysicalLowBounds.pressureTerm (amp slope : ℝ) (M : Matrix) (r w : EulerSmoothLimit.Space) : Matrix

Pressure term, given by (-2*amp*⟪r,M w⟫_ℝ*slope/‖r‖^2) • rankOne ℝ r r.

Equations

• EulerPacketPhysicalLowBounds.pressureTerm amp slope M r w = (-2 * amp * inner ℝ r (M w) * slope / ‖r‖ ^ 2) • ((InnerProductSpace.rankOne ℝ) r) r

theorem EulerPacketPhysicalLowBounds.profile_deriv_abs (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (θ : ℝ) : |deriv (EulerPeriodicProfile.profile δ) θ| ≤ δ⁻¹

theorem EulerPacketPhysicalLowBounds.flux_abs_le (M : Matrix) (r w : EulerSmoothLimit.Space) : |inner ℝ r (M w)| ≤ ‖M‖ * (‖r‖ * ‖w‖)

theorem EulerPacketPhysicalLowBounds.quadratic_le_norm (M : Matrix) (z : EulerSmoothLimit.Space) : inner ℝ (M z) z ≤ ‖M‖ * ‖z‖ ^ 2

theorem EulerPacketPhysicalLowBounds.shearTerm_norm (amp slope : ℝ) (r w : EulerSmoothLimit.Space) : ‖shearTerm amp slope r w‖ = |amp| * |slope| * (‖r‖ * ‖w‖)

theorem EulerPacketPhysicalLowBounds.pressureTerm_norm (amp slope : ℝ) (M : Matrix) (r w : EulerSmoothLimit.Space) : ‖pressureTerm amp slope M r w‖ = 2 * |amp| * |inner ℝ r (M w)| * |slope|

theorem EulerPacketPhysicalLowBounds.shearTerm_norm_le (amp slope δ : ℝ) (r w : EulerSmoothLimit.Space) (hamp : 0 ≤ amp) (hslope : |slope| ≤ δ⁻¹) : ‖shearTerm amp slope r w‖ ≤ amp * (‖r‖ * ‖w‖) / δ

theorem EulerPacketPhysicalLowBounds.pressureTerm_norm_le (amp slope δ : ℝ) (M : Matrix) (r w : EulerSmoothLimit.Space) (hamp : 0 ≤ amp) (hslope : |slope| ≤ δ⁻¹) : ‖pressureTerm amp slope M r w‖ ≤ 2 * ‖M‖ * (amp * (‖r‖ * ‖w‖)) / δ

theorem EulerPacketPhysicalLowBounds.pressureTerm_quadratic (amp slope : ℝ) (M : Matrix) (r w z : EulerSmoothLimit.Space) : inner ℝ ((pressureTerm amp slope M r w) z) z = -2 * amp * inner ℝ r (M w) * slope * (inner ℝ r z ^ 2 / ‖r‖ ^ 2)

theorem EulerPacketPhysicalLowBounds.normal_projection_quadratic_le (r z : EulerSmoothLimit.Space) : inner ℝ r z ^ 2 / ‖r‖ ^ 2 ≤ ‖z‖ ^ 2

theorem EulerPacketPhysicalLowBounds.pressureTerm_nonpos (amp slope : ℝ) (M : Matrix) (r w z : EulerSmoothLimit.Space) (hamp : 0 ≤ amp) (hslope : 0 ≤ slope) (hflux : 0 ≤ inner ℝ r (M w)) : inner ℝ ((pressureTerm amp slope M r w) z) z ≤ 0

theorem EulerPacketPhysicalLowBounds.pressureTerm_upper_flux (amp slope : ℝ) (M : Matrix) (r w z : EulerSmoothLimit.Space) (hamp : 0 ≤ amp) (hslope : -1 ≤ slope) (hflux : 0 ≤ inner ℝ r (M w)) : inner ℝ ((pressureTerm amp slope M r w) z) z ≤ 2 * amp * inner ℝ r (M w) * ‖z‖ ^ 2

theorem EulerPacketPhysicalLowBounds.pressureTerm_upper (amp slope : ℝ) (M : Matrix) (r w z : EulerSmoothLimit.Space) (hamp : 0 ≤ amp) (hslope : -1 ≤ slope) (hflux : 0 ≤ inner ℝ r (M w)) : inner ℝ ((pressureTerm amp slope M r w) z) z ≤ 2 * ‖M‖ * (amp * (‖r‖ * ‖w‖)) * ‖z‖ ^ 2

theorem EulerPacketPhysicalLowBounds.norm_of_remainder (A B Q : Matrix) (e : ℝ) (he : ‖A - B - Q‖ ≤ e) : ‖A‖ ≤ ‖B‖ + ‖Q‖ + e

theorem EulerPacketPhysicalLowBounds.quadratic_of_remainder (A B Q : Matrix) (e K C : ℝ) (he : ‖A - B - Q‖ ≤ e) (hB : ∀ (z : EulerSmoothLimit.Space), inner ℝ (B z) z ≤ K * ‖z‖ ^ 2) (hQ : ∀ (z : EulerSmoothLimit.Space), inner ℝ (Q z) z ≤ C * ‖z‖ ^ 2) (z : EulerSmoothLimit.Space) : inner ℝ (A z) z ≤ (K + C + e) * ‖z‖ ^ 2

theorem EulerPacketPhysicalLowBounds.good_step_bounds (A B H J M : Matrix) (r w : EulerSmoothLimit.Space) (amp δ θ ev ep V P K size : ℝ) (hamp : 0 ≤ amp) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hsize : amp * (‖r‖ * ‖w‖) ≤ δ * size) (hM : ‖M‖ ≤ V) (hB : ‖B‖ ≤ P) (hJ : ‖J‖ ≤ K) (hev : ‖A - B - shearTerm amp (deriv (EulerPeriodicProfile.profile δ) θ) r w‖ ≤ ev) (hep : ‖H - J - pressureTerm amp (deriv (EulerPeriodicProfile.profile δ) θ) M r w‖ ≤ ep) (hflux : 0 ≤ inner ℝ r (M w)) (Kupper : ℝ) (hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ (J z) z ≤ Kupper * ‖z‖ ^ 2) : ‖A‖ ≤ P + size + ev ∧ ‖H‖ ≤ K + 2 * V * size + ep ∧ ∀ (z : EulerSmoothLimit.Space), inner ℝ (H z) z ≤ (Kupper + 2 * V * δ * size + ep) * ‖z‖ ^ 2

On a good interval the upper pressure cost uses ampsize, whereas absolute velocity and Hessian costs use ampsize/delta.

theorem EulerPacketPhysicalLowBounds.absolute_step_bounds (A B H J M : Matrix) (r w : EulerSmoothLimit.Space) (amp δ θ ev ep V P K size : ℝ) (hamp : 0 ≤ amp) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hsize : amp * (‖r‖ * ‖w‖) ≤ δ * size) (hM : ‖M‖ ≤ V) (hB : ‖B‖ ≤ P) (hJ : ‖J‖ ≤ K) (hev : ‖A - B - shearTerm amp (deriv (EulerPeriodicProfile.profile δ) θ) r w‖ ≤ ev) (hep : ‖H - J - pressureTerm amp (deriv (EulerPeriodicProfile.profile δ) θ) M r w‖ ≤ ep) (Kupper : ℝ) (hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ (J z) z ≤ Kupper * ‖z‖ ^ 2) : ‖A‖ ≤ P + size + ev ∧ ‖H‖ ≤ K + 2 * V * size + ep ∧ ∀ (z : EulerSmoothLimit.Space), inner ℝ (H z) z ≤ (Kupper + 2 * V * size + ep) * ‖z‖ ^ 2

Without a sign assertion the same absolute estimate controls the positive Hessian cost. This is used on history and early forward times.