Related estimates used together by the same construction modules.

The actual correction energy right-hand side has the scalar shrinking-radius form, including its exact zero initial trace.

theorem EulerCorrectionEnergyScalar.correctionRhs_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (Rdot : C(↑(Set.Icc 0 T), ℝ)) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (t : ↑(Set.Icc 0 T)) : have X := (EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t; have Y := (EulerEnergyMetricPaths.lossPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t; have C := EulerCorrectionEnergyMajorants.combinedConstant period S K; (EulerCorrectionMildEnergy.correctionRhs period S hN K Rdot e) t ≤ C * (X + X ^ 2 + S.residual) + (Rdot t / R t + C * ((R t)⁻¹ + S.Rc) * (S.B0 + X)) * Y

The actual scalar correction right-hand side is bounded by the source's nonlinear shrinking-radius expression.

theorem EulerCorrectionEnergyScalar.energyNorm_zero (period : ℝ) [Fact (0 < period)] {q : ℕ} (N : ℕ) (hN : N + 6 ≤ q) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) : EulerGevreyMetricEstimate.energyNorm period N hN ρ K 0 = 0

Zero is exactly zero in the genuine finite metric energy.

theorem EulerCorrectionEnergyScalar.zero_mild_trace (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), e t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) 0 + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) : e ⟨0, ⋯⟩ = 0

The actual zero-initial mild formula has zero trace, without a separately assumed initial-value identity.

theorem EulerCorrectionEnergyScalar.affine_radius_derivative (T : ℝ) (hT : 0 ≤ T) (R Rdot : C(↑(Set.Icc 0 T), ℝ)) (ρ0 A : ℝ) (hR : ∀ (t : ↑(Set.Icc 0 T)), R t = ρ0 - A * ↑t) (hRdot : ∀ (t : ↑(Set.Icc 0 T)), Rdot t = -A) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T hT R) (EulerVolterraConvolution.extendPath T hT Rdot t) t

A prescribed affine radius has its genuine time derivative at every interior point after clamped extension.

Shrinking-radius Gevrey bootstrap from actual integral energy inequalities, including zero norms.

theorem EulerIntegralEnergyBootstrap.liminf_slope_le_of_integral (X A : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hA : ContinuousOn A (Set.Icc a b)) (hineq : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, x ≤ y → X y - X x ≤ ∫ (s : ℝ) in x..y, A s) (x : ℝ) (hx : x ∈ Set.Ico a b) (r : ℝ) (hr : A x < r) : ∃ᶠ (y : ℝ) in nhdsWithin x (Set.Ioi x), slope X x y < r

An all-subinterval integral upper bound gives the genuine right Dini slope bound. The energy itself need only be continuous, and may vanish.

theorem EulerIntegralEnergyBootstrap.close_integral_energy_estimate (X A Y : ℝ → ℝ) (C B Δ r ρ₀ S R₀ : ℝ) (hC : 0 < C) (hB : 0 ≤ B) (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1) (hr : 0 < r) (hρ : 0 < ρ₀) (hS : 0 ≤ S) (hR : 0 ≤ R₀) (hdecay : 2 * C * (B + Δ) * S ≤ ρ₀ / 2) (hscale : ρ₀ * R₀ ≤ 1) (hsmall : 2 * r * Real.exp (3 * C * S) ≤ Δ / 2) (hcont : ContinuousOn X (Set.Icc 0 S)) (hAcont : ContinuousOn A (Set.Icc 0 S)) (hinit : X 0 ≤ 2 * r) (hint : ∀ s ∈ Set.Icc 0 S, ∀ t ∈ Set.Icc 0 S, s ≤ t → X t - X s ≤ ∫ (u : ℝ) in s..t, A u) (hY : ∀ t ∈ Set.Ico 0 S, 0 ≤ Y t) (hineq : ∀ t ∈ Set.Ico 0 S, A t ≤ C * (X t + X t ^ 2 + r) + (-2 * C * (B + Δ) / (ρ₀ - 2 * C * (B + Δ) * t) + C * ((ρ₀ - 2 * C * (B + Δ) * t)⁻¹ + R₀) * (B + X t)) * Y t) (t : ℝ) : t ∈ Set.Icc 0 S → X t ≤ 2 * r * Real.exp (3 * C * t) ∧ X t ≤ Δ / 2

The source's nonlinear shrinking-radius bootstrap closes directly from the all-subinterval integral energy bound.