PathDerivative

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

The response derivative along the whole perturbation path

The provider Provider.Path.responseJ_derivative differentiates the scalar response t ↦ J(U, a + t h, p, q) only at the base point t = 0. The J sensitivity proof needs the derivative at every point of the segment [0,1]. As in Provider.Lambda.PathGronwall (which does this for the pure-flux loading p = 0), the path semigroup (a + t h) + s h = a + (t + s) h transports the base-point statement to an arbitrary base point; the present module records the general (p, q) version.

The second declaration is the elementary "mean-value" step used to integrate the resulting differential inequality: a uniform bound on the derivative over [0,1] bounds the increment.

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

Differentiability at every point of the path

theorem Algsuperdiff.Section24.Sensitivity.Provider.Response.hasDerivAt_responseJ_perturbCoeffOn_pair {d : ℕ} (dimension : 2 ≤ d) (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (p q : HCPolySupport.Vec d) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U a h τ) p q) (1 / 2 * HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative U (Frozen.Section24.perturbCoeffOn U a h t) ↑h) (p, -q))) t

The scalar response is differentiable at every point of the perturbation path, with derivative one half of the D_h quadratic form at the current base point tested against (p, -q).

This is the derivative theorem Provider.Path.responseJ_derivative transported along the path semigroup, exactly as in Provider.Lambda.PathGronwall.hasDerivAt_responseJ_perturbCoeffOn, but for a general loading (p, q) rather than the pure-flux loading p = 0.

Integrating a uniform derivative bound

theorem Algsuperdiff.Section24.Sensitivity.Provider.Response.le_add_of_hasDerivAt_le {y y' : ℝ → ℝ} {B t₁ t₂ : ℝ} (hderiv : ∀ (τ : ℝ), HasDerivAt y (y' τ) τ) (hbound : ∀ (τ : ℝ), t₁ ≤ τ → τ ≤ t₂ → y' τ ≤ B) (ht : t₁ ≤ t₂) : y t₂ ≤ y t₁ + B * (t₂ - t₁)

The increment of a differentiable function is controlled by a uniform bound on its derivative. This is the elementary integration step behind the source's passage from the pointwise derivative bound to the self-referential inequality for the maximum of J along the segment.