Closure

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

The response derivative along the canonical perturbation path

This module assembles the provider theorem responseJ_derivative:

• the deterministic identity J(U,p,q;a) = mu(U,(-p,q);a) - p·q reduces the scalar response path to the doubled-mu path;
• the upper second-difference expansion at the base minimizer gives the O(t²) one-sided bound with slope ℓ(X₀);
• the lower expansion at the perturbed minimizer gives the opposite bound with slope ℓ(X_t), and minimizer continuity turns the discrepancy into |t| · O(√|t|);
• the D_h identification ℓ(X₀) = ½ (p,-q)·D_h(U;a)(p,-q) identifies the slope with the frozen value.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.hasDerivAt_doubledMu_perturbCoeffOn {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (p q : HCPolySupport.Vec d) {X0 : HCPolySupport.Book.Ch02.DoubledField d} (hX0 : HCPolySupport.Book.Ch02.IsDoubledMuMinimizer U a (-p, q) X0) : HasDerivAt (fun (t : ℝ) => HCPolySupport.Book.Ch02.doubledMu U (Frozen.Section24.perturbCoeffOn U a h t) (-p, q)) (pathLinearTerm a (↑↑h) X0) 0

Differentiability of the doubled-mu path at the base point. The slope is the linear response term of any base minimizer.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.responseJ_derivative {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) : HasDerivAt (fun (t : ℝ) => HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U a h t) p q) (1 / 2 * HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative U a ↑h) (p, -q))) 0

Provider theorem: the response derivative along the canonical perturbation path. The scalar response functional is differentiable at the base coefficient in the direction of any bounded skew perturbation, with derivative ½ (p,-q) · D_h(U;a) (p,-q).