PathGronwall

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

The pure-flux response along the canonical perturbation path

Source: ABK26. The conditional lambda_{s,q} sensitivity estimate compounds a per-cube estimate along the segment a + t h, t ∈ [0,1]. This module supplies the two facts about that segment that the compounding needs, at a general Chapter 2 domain and for the pure-flux loading p = 0:

• the perturbation path is a one-parameter semigroup, `(a + t h) + s h = a + (t
  • s) h, so the derivative theorem Provider.Path.responseJ_derivative— which differentiates only at the base point — yields differentiability oft ↦ J(U, a + t h, 0, q)at *every*t, with derivative the D_h` flux form at the current base point;
• a Grönwall step: a pointwise bound |y'| ≤ K y on an interval turns into the multiplicative bound y t₂ ≤ exp (K (t₂ - t₁)) * y t₁.

Nothing in this module asserts differentiability of any multiscale aggregate; only the single-cube scalar response is differentiated, exactly as required by the aggregation argument.

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

The perturbation path is a semigroup

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.perturbCoeffOn_perturbCoeffOn {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t s : ℝ) : (Frozen.Section24.perturbCoeffOn U (Frozen.Section24.perturbCoeffOn U a h t) h s).AEEq (Frozen.Section24.perturbCoeffOn U a h (t + s))

The canonical perturbation path is additive in its parameter.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.responseJ_perturbCoeffOn_add {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t s : ℝ) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U (Frozen.Section24.perturbCoeffOn U a h t) h s) p q = HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U a h (t + s)) p q

The pure-flux response along the path is unchanged by reparametrizing the base point.

The D_h flux form

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.dhFluxForm {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (q : HCPolySupport.Vec d) : ℝ

The D_h quadratic form at the pure-flux loading P = (0, -q). This is the bottom-right entry of D_h tested against q, i.e. the slope of the pure-flux response along the perturbation path.

Equations

• One or more equations did not get rendered due to their size.

Differentiability of the pure-flux response along the whole path

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.hasDerivAt_responseJ_perturbCoeffOn {d : ℕ} (dimension : 2 ≤ d) (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (q : HCPolySupport.Vec d) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U a h τ) 0 q) (1 / 2 * dhFluxForm U (Frozen.Section24.perturbCoeffOn U a h t) h q) t

The pure-flux response is differentiable at every point of the perturbation path, with derivative one half of the D_h flux form at the current base point. This is the derivative theorem transported along the path semigroup.

The Grönwall step

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.le_exp_mul_of_hasDerivAt_le {y y' : ℝ → ℝ} {K t₁ t₂ : ℝ} (hderiv : ∀ (τ : ℝ), HasDerivAt y (y' τ) τ) (hbound : ∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → y' τ ≤ K * y τ) (ht : t₁ ≤ t₂) : y t₂ ≤ Real.exp (K * (t₂ - t₁)) * y t₁

Grönwall on an interval. A nonnegative differentiable function whose derivative is bounded by K times its value grows at most exponentially.