Bootstrap

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The self-referential bootstrap along the perturbation path

Source: ABK26. At the gauge exponents (s,q) = (3/8, 2) the per-cube sensitivity estimate is self-referential: the growth rate of the coarse gauge along the path a + t h is proportional to the coarse gauge itself. The source integrates the resulting Riccati inequality; that step presupposes differentiability of an infinite weighted aggregate of finite maxima and is therefore replaced here.

This module contains the gauge-free arithmetic of the replacement. The input is an abstract ratio engine

(∀ tau ∈ [t₁, t₂], Psi tau ≤ C)  ⟹  Psi t₂ ≤ exp (K C (t₂ - t₁)) * Psi t₁ ,

which is what a Grönwall estimate for the single-cube responses plus the descendant aggregation produces, together with a crude uniform bound on Psi over [0,1]. Neither continuity nor differentiability of Psi is assumed.

The engine is run on a grid of mesh T/N with N chosen so large that the crude bound only costs a factor 2 on one mesh interval. On such an interval the engine can be re-run with the sharp local bound 2 Psi (t_k), which turns the exponential into the discrete Riccati step Psi (t_{k+1}) ≤ (1 + (4 K T / N) Psi (t_k)) Psi (t_k) handled by Multiscale.riccati_step_le. The crude bound therefore never enters the conclusion.

Every declaration is an internal helper for the Section 2.4 sensitivity providers.

Elementary exponential bounds

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.exp_half_le_two : Real.exp (1 / 2) ≤ 2

exp (1/2) ≤ 2.

The bootstrap

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.le_riccati_of_ratio_engine {Ψ : ℝ → ℝ} {K B : ℝ} (hΨ : ∀ (t : ℝ), 0 ≤ Ψ t) (hK : 0 ≤ K) (hB : 0 ≤ B) (hcrude : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → Ψ t ≤ B) (hengine : ∀ (t₁ t₂ C : ℝ), 0 ≤ t₁ → t₁ ≤ t₂ → t₂ ≤ 1 → (∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → Ψ τ ≤ C) → Ψ t₂ ≤ Real.exp (K * C * (t₂ - t₁)) * Ψ t₁) (hsmall : 4 * K * Ψ 0 < 1) {T : ℝ} (hT0 : 0 ≤ T) (hT1 : T ≤ 1) : Ψ T ≤ Ψ 0 / (1 - 4 * K * Ψ 0)

The self-referential bootstrap.

Let Psi ≥ 0 satisfy the ratio engine hengine and admit some finite bound B on [0,1]. If the initial value satisfies the smallness gate 4 K Psi 0 < 1, then Psi obeys the Riccati bound Psi T ≤ Psi 0 / (1 - 4 K Psi 0) on all of [0,1], with a constant that does not involve B.

The closed conclusion

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.le_one_add_four_mul_of_ratio_engine {Ψ Y : ℝ → ℝ} {K B : ℝ} (hΨ : ∀ (t : ℝ), 0 ≤ Ψ t) (hK : 0 ≤ K) (hB : 0 ≤ B) (hY : 0 ≤ Y 0) (hcrude : ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → Ψ t ≤ B) (hengine : ∀ (t₁ t₂ C : ℝ), 0 ≤ t₁ → t₁ ≤ t₂ → t₂ ≤ 1 → (∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → Ψ τ ≤ C) → Ψ t₂ ≤ Real.exp (K * C * (t₂ - t₁)) * Ψ t₁) (hengineY : ∀ (C : ℝ), (∀ (τ : ℝ), 0 ≤ τ → τ ≤ 1 → Ψ τ ≤ C) → Y 1 ≤ Real.exp (K * C) * Y 0) (hsmall : 4 * K * Ψ 0 ≤ 1 / 2) : Y 1 ≤ (1 + 4 * K * Ψ 0) * Y 0

The closed form of the bootstrap. Under the smallness gate 4 K Psi 0 ≤ 1/2, the aggregate ratio produced by the engine over the whole segment is at most 1 + 4 K Psi 0.