DiscreteCompounding

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

Discrete compounding arithmetic for the Section 2.4 sensitivity estimates

The manuscript's Section 2.4 sensitivity proofs are written as differential inequalities in the segment parameter t for a + t h. The aggregate coarse-grained quantities lambda_{s,q}^{-1} and Lambda_{s,q} are infinite weighted aggregates of finite maxima of one-cube observables, so they are not classically differentiable in t, and no such regularity may be assumed. Every t-derivative step of the source is therefore replaced here by a purely discrete compounding argument along the path a + (k/N) h, k = 0, …, N.

This module contains only the gauge-free real-analysis arithmetic behind that replacement:

• riccati_step_le — the discrete replacement for integrating the Riccati inequality y' ≤ K y² obtained at the self-referential gauge (s,q) = (3/8,2), giving the source's y 0 / (1 - K * y 0) bound;
• mul_sqrt_mul_sqrt_le_young, absorb_sqrt_self_bound, self_bound_le_closed — the Young-inequality absorption turning M ≤ J + c √E √M + r M (with r small) into a closed bound, which is the arithmetic content of the display of ABK26.

Elementary exponential comparisons

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.inv_one_sub_le_one_add_two_mul {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1 / 2) : (1 - x)⁻¹ ≤ 1 + 2 * x

(1 - x)⁻¹ ≤ 1 + 2 x on [0, 1/2].

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.exp_le_one_add_two_mul {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1 / 2) : Real.exp x ≤ 1 + 2 * x

exp x ≤ 1 + 2 x on [0, 1/2].

The discrete Riccati step

At the self-referential gauge (s,q) = (3/8,2) the per-step ratio itself involves the current value, so the compounding above is not directly available. The source integrates the resulting Riccati inequality; the discrete analogue below is exact and needs no differentiability.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.riccati_step_le {y : ℕ → ℝ} {K : ℝ} (N : ℕ) (hy : ∀ (k : ℕ), 0 ≤ y k) (hK : 0 ≤ K) (hu : K * y 0 < 1) (hstep : ∀ k < N, y (k + 1) ≤ (1 + K / ↑N * y k) * y k) : y N ≤ y 0 / (1 - K * y 0)

Discrete integration of the Riccati inequality y (k+1) ≤ (1 + (K/N) y k) y k. This is the discrete form of the source's bound y 0 / (1 - K y 0).

Young absorption of a self-referential bound

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.mul_sqrt_mul_sqrt_le_young {c E M δ : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M) (hδ : 0 < δ) : c * √E * √M ≤ δ / 4 * M + δ⁻¹ * c ^ 2 * E

Young's inequality in the form used by the absorption step: c √E √M ≤ (δ/4) M + δ⁻¹ c² E.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.absorb_sqrt_self_bound {M J E c r δ : ℝ} (hM : 0 ≤ M) (hE : 0 ≤ E) (hδ : 0 < δ) (hbound : M ≤ J + c * √E * √M + r * M) : (1 - δ / 4 - r) * M ≤ J + δ⁻¹ * c ^ 2 * E

Absorption of the self-referential bound M ≤ J + c √E √M + r M into (1 - δ/4 - r) M ≤ J + δ⁻¹ c² E.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.self_bound_le_closed {M J E c r δ : ℝ} (hM : 0 ≤ M) (hJ : 0 ≤ J) (hE : 0 ≤ E) (hr : 0 ≤ r) (hr' : r ≤ 1 / 4) (hδ : 0 < δ) (hδ' : δ ≤ 1) (hbound : M ≤ J + c * √E * √M + r * M) : M ≤ (1 + δ + 2 * r) * J + 2 * δ⁻¹ * c ^ 2 * E

The closed form of the absorption step. Under the smallness condition r ≤ 1/4 and for 0 < δ ≤ 1, a self-referential bound M ≤ J + c √E √M + r M yields M ≤ (1 + δ + 2 r) J + 2 δ⁻¹ c² E.