Uniform comparison of ideal primary sizes before target. This follows from the actual scalar equation's prefix and weighted monotonicity.

noncomputable def EulerPacketMovingFrame.idealPrimarySize (σ : ℝ) (Z : ℝ → ℝ) (t : ℝ) : ℝ

Ideal primary size, given by Real.sqrt (1+(σ^2*t^2)^2)*Z t.

Equations

• EulerPacketMovingFrame.idealPrimarySize σ Z t = √(1 + (σ ^ 2 * t ^ 2) ^ 2) * Z t

theorem EulerPacketMovingFrame.quadratic_weight_sqrt {p : ℝ} (hp : 0 ≤ p) : √(1 + p ^ 2) ≤ 1 + p ∧ 1 + p ≤ 2 * √(1 + p ^ 2)

theorem EulerPacketMovingFrame.equation30_polynomial_size_monotone {σ : ℝ} {Z Z₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) : MonotoneOn (fun (t : ℝ) => (1 + σ ^ 2 * t ^ 2) * Z t) (Set.Ici 0)

theorem EulerPacketMovingFrame.equation30_ideal_size_comparison {σ s t : ℝ} {Z Z₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) (hs : 0 ≤ s) (hst : s ≤ t) : idealPrimarySize σ Z s ≤ 2 * idealPrimarySize σ Z t

The ideal physical primary size is bounded by twice its later size, uniformly in the initial nonnegative scalar slope.