Order estimates for the scalar ODE occurring in equation (30) of the proposed Euler packet argument. These are finite-dimensional ODE results only.

theorem EulerPacketGrowth.pair_nonneg_of_strict_boundary {f g df dg : ℝ → ℝ} {T : ℝ} (hf : ∀ t ∈ Set.Icc 0 T, HasDerivAt f (df t) t) (hg : ∀ t ∈ Set.Icc 0 T, HasDerivAt g (dg t) t) (hf0 : 0 ≤ f 0) (hg0 : 0 ≤ g 0) (hboundary : ∀ t ∈ Set.Ico 0 T, 0 ≤ f t → 0 ≤ g t → (f t = 0 → 0 < df t) ∧ (g t = 0 → 0 < dg t)) (t : ℝ) : t ∈ Set.Icc 0 T → 0 ≤ f t ∧ 0 ≤ g t

Two differentiable functions remain nonnegative if every boundary point of the nonnegative quadrant has a strictly inward derivative.

theorem EulerPacketGrowth.cooperative_nonneg_of_bounded {f g df dg a b : ℝ → ℝ} {T K : ℝ} (hf : ∀ t ∈ Set.Icc 0 T, HasDerivAt f (df t) t) (hg : ∀ t ∈ Set.Icc 0 T, HasDerivAt g (dg t) t) (hf0 : 0 ≤ f 0) (hg0 : 0 ≤ g 0) (ha : ∀ t ∈ Set.Icc 0 T, 0 ≤ a t ∧ a t ≤ K) (hb : ∀ t ∈ Set.Icc 0 T, 0 ≤ b t ∧ b t ≤ K) (hdf : ∀ t ∈ Set.Icc 0 T, a t * g t ≤ df t) (hdg : ∀ t ∈ Set.Icc 0 T, b t * f t ≤ dg t) (t : ℝ) : t ∈ Set.Icc 0 T → 0 ≤ f t ∧ 0 ≤ g t

Positivity for a cooperative pair of differential inequalities. The nonnegative quadrant is invariant; positivity is not an additional hypothesis.

theorem EulerPacketGrowth.cooperative_nonneg {f g df dg a b : ℝ → ℝ} {T : ℝ} (hf : ∀ t ∈ Set.Icc 0 T, HasDerivAt f (df t) t) (hg : ∀ t ∈ Set.Icc 0 T, HasDerivAt g (dg t) t) (hf0 : 0 ≤ f 0) (hg0 : 0 ≤ g 0) (ha : ∀ t ∈ Set.Icc 0 T, 0 ≤ a t ∧ a t ≤ 2) (hb : ∀ t ∈ Set.Icc 0 T, 0 ≤ b t ∧ b t ≤ 2) (hdf : ∀ t ∈ Set.Icc 0 T, a t * g t ≤ df t) (hdg : ∀ t ∈ Set.Icc 0 T, b t * f t ≤ dg t) (t : ℝ) : t ∈ Set.Icc 0 T → 0 ≤ f t ∧ 0 ≤ g t

A specialization of cooperative positivity with coefficient bound 2.

theorem EulerPacketGrowth.cosh_lower_of_flux_system {V F D c : ℝ → ℝ} {T : ℝ} (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (F t / D t) t) (hF : ∀ t ∈ Set.Icc 0 T, HasDerivAt F (c t * V t) t) (hV0 : V 0 = 1) (hF0 : 0 ≤ F 0) (hD : ∀ t ∈ Set.Icc 0 T, 1 ≤ D t ∧ D t ≤ 2) (hc : ∀ t ∈ Set.Icc 0 T, 1 ≤ c t ∧ c t ≤ 2) (t : ℝ) : t ∈ Set.Icc 0 T → Real.cosh (t / √2) ≤ V t ∧ √2 * Real.sinh (t / √2) ≤ F t

The flux system V' = F/D, F' = c V dominates the constant-coefficient system with D = 2 and c = 1. In particular, its solution is positive and has a hyperbolic-cosine lower bound, for every nonnegative initial flux.

theorem EulerPacketGrowth.equation30_cosh_lower {β T : ℝ} {V V₁ : ℝ → ℝ} (hβ : 0 ≤ β) (hβsmall : β ≤ 1 / 2) (hT : 0 ≤ T) (hscale : β * T ^ 2 ≤ 1) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (V₁ t) t) (hflux : ∀ t ∈ Set.Icc 0 T, HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * V₁ s) (2 * (1 - β * (β * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : t ∈ Set.Icc 0 T → Real.cosh (t / √2) ≤ V t ∧ √2 * Real.sinh (t / √2) ≤ (1 + (β * t ^ 2) ^ 2) * V₁ t

The precise cosine-hyperbolic growth comparison used after equation (30). The initial derivative is allowed to be arbitrarily large and nonnegative.

theorem EulerPacketGrowth.equation30_positive {β T : ℝ} {V V₁ : ℝ → ℝ} (hβ : 0 ≤ β) (hβsmall : β ≤ 1 / 2) (hT : 0 ≤ T) (hscale : β * T ^ 2 ≤ 1) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (V₁ t) t) (hflux : ∀ t ∈ Set.Icc 0 T, HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * V₁ s) (2 * (1 - β * (β * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : t ∈ Set.Icc 0 T → 0 < V t ∧ 0 ≤ V₁ t

Equation (30) gives positivity and a nonnegative derivative from the initial conditions alone, throughout the pre-inversion interval.

theorem EulerPacketGrowth.exp_quarter_le_cosh {t : ℝ} (ht : 4 ≤ t) : Real.exp (t / 4) ≤ Real.cosh (t / √2)

A convenient pure exponential consequence of the hyperbolic-cosine bound.

theorem EulerPacketGrowth.equation30_endpoint_exponential {β : ℝ} {V V₁ : ℝ → ℝ} (hβ : 0 < β) (hβsmall : β ≤ 1 / 16) (hV : ∀ t ∈ Set.Icc 0 (1 / √β), HasDerivAt V (V₁ t) t) (hflux : ∀ t ∈ Set.Icc 0 (1 / √β), HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * V₁ s) (2 * (1 - β * (β * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) : Real.exp (1 / (4 * √β)) ≤ V (1 / √β)

At T = 1 / sqrt β, equation (30) amplifies by at least exp (1 / (4 sqrt β)), uniformly over every nonnegative initial derivative.

theorem EulerPacketGrowth.flux_lower_initial {V F D c : ℝ → ℝ} {T K : ℝ} (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (F t / D t) t) (hF : ∀ t ∈ Set.Icc 0 T, HasDerivAt F (c t * V t) t) (hV0 : 0 ≤ V 0) (hF0 : 0 ≤ F 0) (hD : ∀ t ∈ Set.Icc 0 T, 0 ≤ 1 / D t ∧ 1 / D t ≤ K) (hc : ∀ t ∈ Set.Icc 0 T, 0 ≤ c t ∧ c t ≤ K) (t : ℝ) : t ∈ Set.Icc 0 T → V 0 ≤ V t ∧ F 0 ≤ F t

Nonnegative initial values give componentwise lower bounds for a cooperative flux system, with no smallness restriction on the coefficients.

theorem EulerPacketGrowth.inversion_positive {β a : ℝ} {f f₁ : ℝ → ℝ} (hβ : 0 < β) (hβsmall : β ≤ 1) (ha : 0 ≤ a) (hf : ∀ y ∈ Set.Icc a 1, HasDerivAt f (f₁ y) y) (hflux : ∀ y ∈ Set.Icc a 1, HasDerivAt (fun (z : ℝ) => (1 + z ^ 4) * f₁ z) ((2 / β - 2 * y ^ 2) * f y) y) (hf1 : 0 < f 1) (hf₁1 : f₁ 1 < 0) (y : ℝ) : y ∈ Set.Icc a 1 → f 1 ≤ f y ∧ 0 < f y ∧ f₁ y < 0

The inverted equation preserves positive f and negative f' when it is integrated from y = 1 towards smaller nonnegative y.

theorem EulerPacketGrowth.riccati_upper_bound {l dl : ℝ → ℝ} {T : ℝ} (hl : ∀ t ∈ Set.Icc 0 T, HasDerivAt l (dl t) t) (hineq : ∀ t ∈ Set.Ico 0 T, dl t ≤ 2 - l t ^ 2) (t : ℝ) : t ∈ Set.Ioc 0 T → l t ≤ 2 + 1 / t

A uniform Riccati upper bound that does not depend on the finite initial value: a solution of l' ≤ 2 - l² obeys l(t) ≤ 2 + 1/t for t > 0.

theorem EulerPacketGrowth.equation30_second_derivative {β t : ℝ} {V V₁ : ℝ → ℝ} (hflux : HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * V₁ s) (2 * (1 - β * (β * t ^ 2)) * V t) t) : HasDerivAt V₁ ((2 * (1 - β * (β * t ^ 2)) * V t - 4 * β ^ 2 * t ^ 3 * V₁ t) / (1 + (β * t ^ 2) ^ 2)) t

Recovering the ordinary second derivative from the differentiated flux.

theorem EulerPacketGrowth.equation30_log_derivative_upper {β T : ℝ} {V V₁ : ℝ → ℝ} (hβ : 0 ≤ β) (hβsmall : β ≤ 1 / 2) (hT : 0 ≤ T) (hscale : β * T ^ 2 ≤ 1) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (V₁ t) t) (hflux : ∀ t ∈ Set.Icc 0 T, HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * V₁ s) (2 * (1 - β * (β * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : t ∈ Set.Ioc 0 T → V₁ t / V t ≤ 2 + 1 / t

The logarithmic derivative in equation (30) is uniformly bounded away from the initial time, independently of the initial nonnegative slope.

theorem EulerPacketGrowth.riccati_le_four {z a b : ℝ → ℝ} {T : ℝ} (hz : ∀ t ∈ Set.Icc 0 T, HasDerivAt z (a t - z t ^ 2 + b t * z t) t) (hz0 : z 0 ≤ 4) (ha : ∀ t ∈ Set.Ico 0 T, a t ≤ 2) (hb : ∀ t ∈ Set.Ico 0 T, b t ≤ 1) (t : ℝ) : t ∈ Set.Icc 0 T → z t ≤ 4

A coarse Riccati upper barrier for the inverted equation.

theorem EulerPacketGrowth.riccati_tracking {z μ dz dμ : ℝ → ℝ} {T ε : ℝ} (hε : 0 < ε) (hz : ∀ t ∈ Set.Icc 0 T, HasDerivAt z (dz t) t) (hμ : ∀ t ∈ Set.Icc 0 T, HasDerivAt μ (dμ t) t) (hzrange : ∀ t ∈ Set.Icc 0 T, 0 ≤ z t ∧ z t ≤ 4) (hμrange : ∀ t ∈ Set.Icc 0 T, 1 ≤ μ t ∧ μ t ≤ 2) (hres : ∀ t ∈ Set.Ico 0 T, |dz t - (μ t ^ 2 - z t ^ 2)| ≤ 20 * ε) (hμderiv : ∀ t ∈ Set.Ico 0 T, |dμ t| ≤ 4 * ε) (t : ℝ) : t ∈ Set.Icc 0 T → |z t - μ t| ≤ 6 * Real.exp (-t) + 48 * ε

Quantitative tracking of the stable positive Riccati branch. This abstract estimate is applied below with μ = sqrt(2/(1+y^4)); all constants are explicit and do not involve the initial nonnegative slope.

theorem EulerPacketGrowth.riccati_tracking_after_layer {z μ dz dμ : ℝ → ℝ} {T ε : ℝ} (hε : 0 < ε) (hz : ∀ t ∈ Set.Icc 0 T, HasDerivAt z (dz t) t) (hμ : ∀ t ∈ Set.Icc 0 T, HasDerivAt μ (dμ t) t) (hzrange : ∀ t ∈ Set.Icc 0 T, 0 ≤ z t ∧ z t ≤ 4) (hμrange : ∀ t ∈ Set.Icc 0 T, 1 ≤ μ t ∧ μ t ≤ 2) (hres : ∀ t ∈ Set.Ico 0 T, |dz t - (μ t ^ 2 - z t ^ 2)| ≤ 20 * ε) (hμderiv : ∀ t ∈ Set.Ico 0 T, |dμ t| ≤ 4 * ε) (t : ℝ) : t ∈ Set.Icc 0 T → 1 / (2 * ε) ≤ t → |z t - μ t| ≤ 60 * ε

After time 1/(2ε) the Riccati tracking error is at most 60ε.

noncomputable def EulerPacketGrowth.riccatiRoot (ε t : ℝ) : ℝ

The positive stationary branch of the rescaled inverted Riccati equation.

Equations

• EulerPacketGrowth.riccatiRoot ε t = √(2 / (1 + (1 - ε * t) ^ 4))

noncomputable def EulerPacketGrowth.riccatiRootDeriv (ε t : ℝ) : ℝ

Its derivative as the spatial coordinate y = 1 - εt decreases.

Equations

• EulerPacketGrowth.riccatiRootDeriv ε t = 4 * ε * (1 - ε * t) ^ 3 / ((1 + (1 - ε * t) ^ 4) ^ 2 * EulerPacketGrowth.riccatiRoot ε t)

theorem EulerPacketGrowth.hasDerivAt_riccatiRoot (ε t : ℝ) : HasDerivAt (riccatiRoot ε) (riccatiRootDeriv ε t) t

theorem EulerPacketGrowth.riccatiRoot_bounds {ε t : ℝ} (hy : 0 ≤ 1 - ε * t ∧ 1 - ε * t ≤ 1) : 1 ≤ riccatiRoot ε t ∧ riccatiRoot ε t ≤ 2

theorem EulerPacketGrowth.riccatiRootDeriv_bounds {ε t : ℝ} (hε : 0 ≤ ε) (hy : 0 ≤ 1 - ε * t ∧ 1 - ε * t ≤ 1) : 0 ≤ riccatiRootDeriv ε t ∧ riccatiRootDeriv ε t ≤ 4 * ε

noncomputable def EulerPacketGrowth.invertedRiccati (ε t z : ℝ) : ℝ

Right-hand side of the inverted Riccati equation in the fast coordinate t = (1-y)/ε, where ε = sqrt β.

Equations

• EulerPacketGrowth.invertedRiccati ε t z = (2 - 2 * ε ^ 2 * (1 - ε * t) ^ 2) / (1 + (1 - ε * t) ^ 4) - z ^ 2 + 4 * ε * (1 - ε * t) ^ 3 / (1 + (1 - ε * t) ^ 4) * z

theorem EulerPacketGrowth.inverted_riccati_squared_error {ε T : ℝ} {z : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hscale : ε * T ≤ 1) (hz : ∀ t ∈ Set.Icc 0 T, HasDerivAt z (invertedRiccati ε t (z t)) t) (hz0 : z 0 ≤ 4) (hzn : ∀ t ∈ Set.Icc 0 T, 0 ≤ z t) (t : ℝ) : t ∈ Set.Icc 0 T → 1 / (2 * ε) ≤ t → |z t ^ 2 - 2 / (1 + (1 - ε * t) ^ 4)| ≤ 360 * ε

Explicit form of the uniform O(sqrt β) Riccati estimate in (31). This theorem uses the exact rescaled ODE and an initial bound of 4; the preceding logarithmic-derivative estimate supplies that bound independently of the nonnegative initial slope.

theorem EulerPacketGrowth.inversion_second_derivative {β y : ℝ} {f f₁ : ℝ → ℝ} (hflux : HasDerivAt (fun (z : ℝ) => (1 + z ^ 4) * f₁ z) ((2 / β - 2 * y ^ 2) * f y) y) : HasDerivAt f₁ (((2 / β - 2 * y ^ 2) * f y - 4 * y ^ 3 * f₁ y) / (1 + y ^ 4)) y

The second derivative of a solution of the inverted scalar equation.

theorem EulerPacketGrowth.hasDerivAt_inverted_logderivative {ε t : ℝ} {f f₁ : ℝ → ℝ} (hε : ε ≠ 0) (hfpos : f (1 - ε * t) ≠ 0) (hf : HasDerivAt f (f₁ (1 - ε * t)) (1 - ε * t)) (hflux : HasDerivAt (fun (y : ℝ) => (1 + y ^ 4) * f₁ y) ((2 / ε ^ 2 - 2 * (1 - ε * t) ^ 2) * f (1 - ε * t)) (1 - ε * t)) : HasDerivAt (fun (s : ℝ) => -ε * f₁ (1 - ε * s) / f (1 - ε * s)) (invertedRiccati ε t (-ε * f₁ (1 - ε * t) / f (1 - ε * t))) t

The exact Riccati equation after the substitutions y = 1-εt and z = -ε f'/f.

theorem EulerPacketGrowth.inversion_riccati_error {ε a : ℝ} {f f₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (ha : 0 ≤ a) (hf : ∀ y ∈ Set.Icc a 1, HasDerivAt f (f₁ y) y) (hflux : ∀ y ∈ Set.Icc a 1, HasDerivAt (fun (z : ℝ) => (1 + z ^ 4) * f₁ z) ((2 / ε ^ 2 - 2 * y ^ 2) * f y) y) (hf1 : 0 < f 1) (hf₁1 : f₁ 1 < 0) (hinit : -ε * f₁ 1 / f 1 ≤ 4) (y : ℝ) : y ∈ Set.Icc a (1 / 2) → |(-ε * f₁ y / f y) ^ 2 - 2 / (1 + y ^ 4)| ≤ 360 * ε

The uniform Riccati estimate directly for solutions of the inverted scalar equation. Positivity on the interval follows from the endpoint conditions; it is not assumed.

noncomputable def EulerPacketGrowth.invertedScalar (ε : ℝ) (V : ℝ → ℝ) (y : ℝ) : ℝ

Inversion of a solution in the original time variable, including the rescaling x = ετ.

Equations

• EulerPacketGrowth.invertedScalar ε V y = V (y⁻¹ / ε) / y

noncomputable def EulerPacketGrowth.invertedScalarDeriv (ε : ℝ) (V V₁ : ℝ → ℝ) (y : ℝ) : ℝ

The exact derivative of invertedScalar, away from y = 0.

Equations

• EulerPacketGrowth.invertedScalarDeriv ε V V₁ y = -V (y⁻¹ / ε) / y ^ 2 - V₁ (y⁻¹ / ε) / (ε * y ^ 3)

theorem EulerPacketGrowth.invertedScalar_equations {ε y : ℝ} {V V₁ : ℝ → ℝ} (hε : ε ≠ 0) (hy : y ≠ 0) (hV : HasDerivAt V (V₁ (y⁻¹ / ε)) (y⁻¹ / ε)) (hflux : HasDerivAt (fun (t : ℝ) => (1 + (ε ^ 2 * t ^ 2) ^ 2) * V₁ t) (2 * (1 - ε ^ 2 * (ε ^ 2 * (y⁻¹ / ε) ^ 2)) * V (y⁻¹ / ε)) (y⁻¹ / ε)) : HasDerivAt (invertedScalar ε V) (invertedScalarDeriv ε V V₁ y) y ∧ HasDerivAt (fun (z : ℝ) => (1 + z ^ 4) * invertedScalarDeriv ε V V₁ z) ((2 / ε ^ 2 - 2 * y ^ 2) * invertedScalar ε V y) y

Both differential equations for the rescaled inversion, derived algebraically from equation (30).

theorem EulerPacketGrowth.invertedScalar_initial_bound {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ t ∈ Set.Icc 0 (1 / ε), HasDerivAt V (V₁ t) t) (hflux : ∀ t ∈ Set.Icc 0 (1 / ε), HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) : 0 < invertedScalar ε V 1 ∧ invertedScalarDeriv ε V V₁ 1 < 0 ∧ -ε * invertedScalarDeriv ε V V₁ 1 / invertedScalar ε V 1 ≤ 4

At the start of inversion the Riccati variable has an absolute bound, independent of the original initial nonnegative slope.

theorem EulerPacketGrowth.equation30_inverted_riccati_error {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (y : ℝ) : 0 < y → y ≤ 1 / 2 → |(-ε * invertedScalarDeriv ε V V₁ y / invertedScalar ε V y) ^ 2 - 2 / (1 + y ^ 4)| ≤ 360 * ε

The full uniform estimate (31) for the scalar equation, including the rescaling, inversion, positivity, and removal of all dependence on the original nonnegative initial slope.

theorem EulerPacketGrowth.flux_wronskian_constant {D c u u₁ v v₁ : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (t : ℝ) : t ∈ Set.Icc a b → u t * (D t * v₁ t) - D t * u₁ t * v t = u a * (D a * v₁ a) - D a * u₁ a * v a

The Wronskian flux of two solutions of (D u')' = c u is conserved.

theorem EulerPacketGrowth.quotient_derivative_of_flux {D c u u₁ v v₁ : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hD : ∀ t ∈ Set.Icc a b, D t ≠ 0) (hupos : ∀ t ∈ Set.Icc a b, u t ≠ 0) (t : ℝ) : t ∈ Set.Icc a b → HasDerivAt (fun (s : ℝ) => v s / u s) ((u a * (D a * v₁ a) - D a * u₁ a * v a) / (D t * u t ^ 2)) t

The derivative of the quotient of two scalar solutions, expressed using their initial Wronskian rather than either exponentially large solution.

theorem EulerPacketGrowth.reduction_of_order {D c u u₁ v v₁ : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hDc : ContinuousOn D (Set.Icc a b)) (hD : ∀ t ∈ Set.Icc a b, D t ≠ 0) (hupos : ∀ t ∈ Set.Icc a b, u t ≠ 0) (t : ℝ) : t ∈ Set.Icc a b → v t = u t * (v a / u a + (u a * (D a * v₁ a) - D a * u₁ a * v a) * ∫ (s : ℝ) in a..t, 1 / (D s * u s ^ 2))

The exact reduction-of-order formula on a closed interval. Its integral contains the reciprocal square of the positive reference solution.

theorem EulerPacketGrowth.invertedScalar_positive {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (y : ℝ) : 0 < y → y ≤ 1 → invertedScalar ε V 1 ≤ invertedScalar ε V y ∧ 0 < invertedScalar ε V y ∧ invertedScalarDeriv ε V V₁ y < 0

Positivity and decrease of the inverted scalar solution for every positive inversion coordinate.

theorem EulerPacketGrowth.equation30_post_inversion_lower {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (x : ℝ) : 1 ≤ x → V (1 / ε) / x ≤ V (x / ε) ∧ 0 < V (x / ε)

Growth remains at least the value at x=1 divided by x after inversion. This is the lower bound used in the exponential gain estimate.

theorem EulerPacketGrowth.equation30_global_positive {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : 0 ≤ t → 0 < V t

A solution with the source's initial conditions stays positive for every nonnegative original time, including beyond the inversion point.

theorem EulerPacketGrowth.equation30_reduction_of_order {ε lam : ℝ} {U U₁ V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV0 : V 0 = 1) (hV₁0 : V₁ 0 = lam) (t : ℝ) : 0 ≤ t → V t = U t * (1 + lam * ∫ (s : ℝ) in 0..t, 1 / ((1 + (ε ^ 2 * s ^ 2) ^ 2) * U s ^ 2))

Reduction of order in the source's normalization V₀(0)=1, V₀'(0)=0, Vλ(0)=1, Vλ'(0)=λ.

theorem EulerPacketGrowth.equation30_zero_slope_prefix_upper {ε : ℝ} {U U₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hU : ∀ t ∈ Set.Icc 0 1, HasDerivAt U (U₁ t) t) (hfluxU : ∀ t ∈ Set.Icc 0 1, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (t : ℝ) : t ∈ Set.Icc 0 1 → U t ≤ Real.exp 3

A fixed upper bound for the zero-slope reference solution on [0,1].

theorem EulerPacketGrowth.equation30_reduction_integral_one_lower {ε : ℝ} {U U₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hU : ∀ t ∈ Set.Icc 0 1, HasDerivAt U (U₁ t) t) (hfluxU : ∀ t ∈ Set.Icc 0 1, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) : 1 / (2 * Real.exp 6) ≤ ∫ (s : ℝ) in 0..1, 1 / ((1 + (ε ^ 2 * s ^ 2) ^ 2) * U s ^ 2)

The reduction-of-order integral at time 1 has a positive absolute lower bound. No numerical approximations occur in the constant.

theorem EulerPacketGrowth.equation30_reduction_integral_lower {ε : ℝ} {U U₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (t : ℝ) : 1 ≤ t → 1 / (2 * Real.exp 6) ≤ ∫ (s : ℝ) in 0..t, 1 / ((1 + (ε ^ 2 * s ^ 2) ^ 2) * U s ^ 2)

The same absolute lower bound holds for the reduction integral at every later time, because its integrand is nonnegative.

theorem EulerPacketGrowth.equation30_slope_uniform_lower {ε lam : ℝ} {U U₁ V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlam : 0 ≤ lam) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hfluxV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hV0 : V 0 = 1) (hV₁0 : V₁ 0 = lam) (t : ℝ) : 1 ≤ t → (1 + lam) / (2 * Real.exp 6) * U t ≤ V t

The solution with slope lam ≥ 0 dominates the zero-slope reference solution by a fixed multiple of (1+lam) after time 1.

theorem EulerPacketGrowth.equation30_prefix_monotone {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) : MonotoneOn V (Set.Icc 0 (1 / ε))

Before x=1, the original scalar solution is nondecreasing.

theorem EulerPacketGrowth.invertedScalar_antitone {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) : AntitoneOn (invertedScalar ε V) (Set.Ioc 0 1)

In inversion coordinates the scalar solution is nonincreasing.

theorem EulerPacketGrowth.equation30_weighted_monotone {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) : MonotoneOn (fun (t : ℝ) => t * V t) (Set.Ici (1 / ε))

After x=1, the product t V(t) is nondecreasing.

theorem EulerPacketGrowth.equation30_relative_ratio {ε Θ : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (s t : ℝ) : 0 ≤ s → s ≤ t → t ≤ Θ → V s ≤ Θ * V t

The reference solution can decrease only by a polynomial factor on a bounded time interval. This is the ratio estimate used in the relative propagator argument.

theorem EulerPacketGrowth.equation30_hasDerivAt_logderivative {ε t : ℝ} {V V₁ : ℝ → ℝ} (hV : HasDerivAt V (V₁ t) t) (hflux : HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hVne : V t ≠ 0) : HasDerivAt (fun (s : ℝ) => V₁ s / V s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) / (1 + (ε ^ 2 * t ^ 2) ^ 2) - 4 * (ε ^ 2) ^ 2 * t ^ 3 / (1 + (ε ^ 2 * t ^ 2) ^ 2) * (V₁ t / V t) - (V₁ t / V t) ^ 2) t

The exact logarithmic-derivative equation wherever the scalar solution does not vanish.

theorem EulerPacketGrowth.equation30_post_inversion_positive_derivative {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : 1 / ε ≤ t → 0 < V t + t * V₁ t

The derivative of t V(t) is strictly positive after inversion.

theorem EulerPacketGrowth.equation30_zero_slope_logderivative_bound {ε : ℝ} {U U₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (t : ℝ) : 0 ≤ t → |U₁ t / U t| ≤ 2

A uniform absolute logarithmic-derivative bound for the zero-slope reference solution, valid on the whole forward interval.

theorem EulerPacketGrowth.reduction_of_order_relative {D c u u₁ v v₁ : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hDc : ContinuousOn D (Set.Icc a b)) (hD : ∀ t ∈ Set.Icc a b, D t ≠ 0) (hupos : ∀ t ∈ Set.Icc a b, u t ≠ 0) (t : ℝ) : t ∈ Set.Icc a b → v t = u t / u a * (v a + D a * (v₁ a - u₁ a / u a * v a) * ∫ (s : ℝ) in a..t, (u a / u s) ^ 2 / D s)

Reduction of order normalized by the reference value at the initial time. This is the form used for relative, rather than absolute, stability.

theorem EulerPacketGrowth.reduction_of_order_derivative_relative {D c u u₁ v v₁ : ℝ → ℝ} {a b : ℝ} (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hD : ∀ t ∈ Set.Icc a b, D t ≠ 0) (hupos : ∀ t ∈ Set.Icc a b, u t ≠ 0) (t : ℝ) : t ∈ Set.Icc a b → v₁ t = u₁ t / u t * v t + u a / u t * D a * (v₁ a - u₁ a / u a * v a) / D t

The derivative counterpart of normalized reduction of order.

theorem EulerPacketGrowth.relative_reduction_integral_bound {D u : ℝ → ℝ} {a b Θ : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ Θ) (hDc : ContinuousOn D (Set.Icc a b)) (huc : ContinuousOn u (Set.Icc a b)) (hD : ∀ s ∈ Set.Icc a b, 1 ≤ D s) (hu : ∀ s ∈ Set.Icc a b, 0 < u s) (hratio : ∀ s ∈ Set.Icc a b, u a ≤ Θ * u s) : 0 ≤ ∫ (s : ℝ) in a..b, (u a / u s) ^ 2 / D s ∧ ∫ (s : ℝ) in a..b, (u a / u s) ^ 2 / D s ≤ Θ ^ 3

A polynomial bound for the normalized reduction integral.

theorem EulerPacketGrowth.relative_propagator_bound {D c u u₁ v v₁ : ℝ → ℝ} {a b Θ : ℝ} (hΘ : 1 ≤ Θ) (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ Θ) (hu : ∀ t ∈ Set.Icc a b, HasDerivAt u (u₁ t) t) (hv : ∀ t ∈ Set.Icc a b, HasDerivAt v (v₁ t) t) (hfu : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * u₁ s) (c t * u t) t) (hfv : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => D s * v₁ s) (c t * v t) t) (hDc : ContinuousOn D (Set.Icc a b)) (hD : ∀ t ∈ Set.Icc a b, 1 ≤ D t ∧ D t ≤ 2 * Θ ^ 4) (hupos : ∀ t ∈ Set.Icc a b, 0 < u t) (hlog : ∀ t ∈ Set.Icc a b, |u₁ t / u t| ≤ 2) (hratio : ∀ t ∈ Set.Icc a b, u a ≤ Θ * u t) : |v b| + |v₁ b| ≤ 20 * Θ ^ 8 * (u b / u a) * (|v a| + |v₁ a|)

A relative propagator estimate with an explicit polynomial loss. The large reference amplitude enters only through u b / u a.

theorem EulerPacketGrowth.equation30_relative_propagator {ε Θ a b : ℝ} {U U₁ Y Y₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (ha : 0 ≤ a) (hab : a ≤ b) (hb : b ≤ Θ) (hU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt U (U₁ t) t) (hfluxU : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * U₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * U t) t) (hU0 : U 0 = 1) (hU₁0 : U₁ 0 = 0) (hY : ∀ t ∈ Set.Icc a b, HasDerivAt Y (Y₁ t) t) (hfluxY : ∀ t ∈ Set.Icc a b, HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Y₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Y t) t) : |Y b| + |Y₁ b| ≤ 20 * Θ ^ 8 * (U b / U a) * (|Y a| + |Y₁ a|)

The ideal scalar propagator has only a polynomial loss relative to the zero-slope growing solution. This proves the reference propagator estimate used before (32), with the explicit constant 20.

theorem EulerPacketGrowth.inverted_riccati_le_four {ε T : ℝ} {z : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hscale : ε * T ≤ 1) (hz : ∀ t ∈ Set.Icc 0 T, HasDerivAt z (invertedRiccati ε t (z t)) t) (hz0 : z 0 ≤ 4) (t : ℝ) : t ∈ Set.Icc 0 T → z t ≤ 4

The coarse upper barrier for the exact inverted Riccati equation.

theorem EulerPacketGrowth.inversion_riccati_range {ε a : ℝ} {f f₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (ha : 0 ≤ a) (hf : ∀ y ∈ Set.Icc a 1, HasDerivAt f (f₁ y) y) (hflux : ∀ y ∈ Set.Icc a 1, HasDerivAt (fun (z : ℝ) => (1 + z ^ 4) * f₁ z) ((2 / ε ^ 2 - 2 * y ^ 2) * f y) y) (hf1 : 0 < f 1) (hf₁1 : f₁ 1 < 0) (hinit : -ε * f₁ 1 / f 1 ≤ 4) (y : ℝ) : y ∈ Set.Icc a 1 → 0 ≤ -ε * f₁ y / f y ∧ -ε * f₁ y / f y ≤ 4

The inverted logarithmic derivative remains in [0,4], derived directly from the scalar equation and its endpoint conditions.

theorem EulerPacketGrowth.equation30_inverted_riccati_range {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (y : ℝ) : 0 < y → y ≤ 1 → 0 ≤ -ε * invertedScalarDeriv ε V V₁ y / invertedScalar ε V y ∧ -ε * invertedScalarDeriv ε V V₁ y / invertedScalar ε V y ≤ 4

The absolute Riccati range for the original scalar initial value problem.

def EulerPacketGrowth.idealFrameNumerator (ε y z : ℝ) : ℝ

The ideal next-frame numerator in inversion coordinates.

Equations

• EulerPacketGrowth.idealFrameNumerator ε y z = -1 + (1 + y ^ 4) * z ^ 2 + ε ^ 2 * y ^ 2 - 2 * ε * z * y ^ 3

def EulerPacketGrowth.idealFrameDenominator (ε y z : ℝ) : ℝ

The ideal next-frame denominator divided by x², where y=1/x.

Equations

• EulerPacketGrowth.idealFrameDenominator ε y z = 1 - ε ^ 2 * y ^ 2 + 2 * ε * z * y ^ 3

theorem EulerPacketGrowth.ideal_frame_identities {ε y z : ℝ} (hy : y ≠ 0) : y⁻¹ ^ 2 + ε ^ 2 + -2 * ε * y⁻¹ * (ε * y - z * y ^ 2) = idealFrameDenominator ε y z / y ^ 2 ∧ -1 + ε ^ 2 * y⁻¹ ^ 2 + (1 + y⁻¹ ^ 4) * (ε * y - z * y ^ 2) ^ 2 + y⁻¹ ^ 2 * (-2 * ε * y⁻¹) * (ε * y - z * y ^ 2) = idealFrameNumerator ε y z

The two exact algebraic identities used for the ideal frame renewal.

theorem EulerPacketGrowth.ideal_frame_bounds {ε y z : ℝ} (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 4) (hy : 0 ≤ y) (hysmall : y ≤ 1 / 2) (hz : 0 ≤ z) (hzupper : z ≤ 4) (herr : |z ^ 2 - 2 / (1 + y ^ 4)| ≤ 360 * ε) : 1 / 2 ≤ idealFrameDenominator ε y z ∧ |idealFrameNumerator ε y z - 1| ≤ 730 * ε ∧ |idealFrameDenominator ε y z / √(1 + y ^ 4) - 1| ≤ y ^ 4 + ε ^ 2 * y ^ 2 + 8 * ε * y ^ 3 ∧ |idealFrameNumerator ε y z / idealFrameDenominator ε y z - 1| ≤ 1500 * ε

Explicit ideal frame-renewal bounds obtained from the Riccati estimate. The constants are deliberately generous absolute constants.

theorem EulerPacketGrowth.equation30_ideal_frame_bounds {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (y : ℝ) : 0 < y → y ≤ 1 / 2 → have z := -ε * invertedScalarDeriv ε V V₁ y / invertedScalar ε V y; 1 / 2 ≤ idealFrameDenominator ε y z ∧ |idealFrameNumerator ε y z - 1| ≤ 730 * ε ∧ |idealFrameDenominator ε y z / √(1 + y ^ 4) - 1| ≤ y ^ 4 + ε ^ 2 * y ^ 2 + 8 * ε * y ^ 3 ∧ |idealFrameNumerator ε y z / idealFrameDenominator ε y z - 1| ≤ 1500 * ε

Ideal frame renewal follows from the scalar initial value problem; the Riccati range and approximation are proved upstream in this file.

theorem EulerPacketGrowth.ideal_target_compression {H ε x : ℝ} (hH : 0 ≤ H) (hε : 0 ≤ ε) (hx : 1 ≤ x) : -2 * H * ε * x ^ 3 / (1 + x ^ 4) ≤ -H * ε / x

The ideal shear contribution to the target-frame compression has the required negative sign and reciprocal target-scale lower magnitude.