PathODE

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

The affine Grönwall step and its Young absorption

Source: ABK26, the integration and Young steps in the proof of e.J.sensitivity.

The manuscript integrates the derivative bound

|∂_t J(t)| ≤ C E^{1/2} M^{1/2} + C ‖∇h‖ λ^{-1} M ,   M = max_{t∈[0,1]} J(t) ,

and then absorbs M by Young's inequality. Formalizing the running maximum M would require a compactness argument; the two lemmas below replace it by an equivalent and strictly elementary route:

• mul_sqrt_le_young_div applies Young's inequality pointwise in t, turning the derivative bound into the affine differential inequality y' ≤ m + c y;
• le_exp_mul_add_of_hasDerivAt_le integrates that inequality exactly, by differentiating the integrating factor e^{-c(t-t₁)} y(t) - m (t - t₁) and observing it is nonincreasing.

The two together give the same closed form as the source: a factor 1 + δ + C ‖∇h‖ λ^{-1} on the base response and a δ^{-1}-weighted energy term.

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.mul_sqrt_le_young_div {A y θ : ℝ} (hy : 0 ≤ y) (hθ : 0 < θ) : A * √y ≤ A ^ 2 / (2 * θ) + θ / 2 * y

Young's inequality in the square-root form.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.le_exp_mul_add_of_hasDerivAt_le {y y' : ℝ → ℝ} {c m t₁ t₂ : ℝ} (hderiv : ∀ (τ : ℝ), HasDerivAt y (y' τ) τ) (hc : 0 ≤ c) (hm : 0 ≤ m) (hbound : ∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → y' τ ≤ m + c * y τ) (ht : t₁ ≤ t₂) : y t₂ ≤ Real.exp (c * (t₂ - t₁)) * (y t₁ + m * (t₂ - t₁))

Exact integration of the affine differential inequality y' ≤ m + c y.

No running maximum and no compactness are used: the integrating factor e^{-c(t-t₁)} y(t) - m (t - t₁) has a nonpositive derivative on [t₁, t₂].