DerivativeBridge

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

Difference-quotient bridge toward responseJ_derivative

Source: (e.derivative.J, with the corrected factor 1/2 frozen in responseJ_derivative).

This module provides the increment calculus that turns the two-sided second-difference expansion into a genuine HasDerivAt, the reduction of the scalar response path to the doubled-mu path via the deterministic identity J(U,p,q;a) = mu(U,(-p,q);a) - p·q, and the nonnegativity of the quadratic path term of an admissible field.

Increment calculus

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.hasDerivAt_of_second_order_bounds {F : ℝ → ℝ} {L K : ℝ} {e : ℝ → ℝ} (he : Filter.Tendsto e (nhds 0) (nhds 0)) (hbound : ∀ (t : ℝ), |F t - F 0 - t * L| ≤ K * t ^ 2 + |t| * e t) : HasDerivAt F L 0

Second-order increment bridge. A one-variable function whose increment matches a linear slope up to K t² + |t| e(t) with e → 0 at 0 is differentiable at 0 with that slope. This is the exact difference quotient shape produced by the two-sided coarse-matrix expansion.

Nonnegativity of the quadratic path term

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecDot_matVecMul_symmPartInv_nonneg {d : ℕ} {lam Lam : ℝ} {A : HCPolySupport.Mat d} (hA : HCPolySupport.IsEllipticMatrix lam Lam A) (ξ : HCPolySupport.Vec d) : 0 ≤ HCPolySupport.vecDot ξ (HCPolySupport.matVecMul (HCPolySupport.symmPart A)⁻¹ ξ)

The inverse of the symmetric part of an elliptic matrix has a nonnegative quadratic form.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.pathQuadraticTerm_nonneg {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (hField : HCPolySupport.CoeffField d) (X : HCPolySupport.Book.Ch02.DoubledField d) : 0 ≤ pathQuadraticTerm a hField X

The quadratic path term of any doubled field is nonnegative.

Reduction of the scalar response path to the doubled-mu path

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.responseJ_perturbCoeffOn_eq_doubledMu_sub {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U a h t) p q = HCPolySupport.Book.Ch02.doubledMu U (Frozen.Section24.perturbCoeffOn U a h t) (-p, q) - HCPolySupport.vecDot p q

The scalar response along the canonical path, written through the deterministic identity J(U,p,q;a) = mu(U,(-p,q);a) - p·q.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.hasDerivAt_responseJ_of_hasDerivAt_doubledMu {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (p q : HCPolySupport.Vec d) {L : ℝ} (hmu : HasDerivAt (fun (t : ℝ) => HCPolySupport.Book.Ch02.doubledMu U (Frozen.Section24.perturbCoeffOn U a h t) (-p, q)) L 0) : HasDerivAt (fun (t : ℝ) => HCPolySupport.Book.Ch02.responseJ U (Frozen.Section24.perturbCoeffOn U a h t) p q) L 0

Differentiability of the doubled-mu path at 0 transfers to the scalar response path, with the same slope.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.doubledMu_perturbCoeffOn_zero {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (P : HCPolySupport.BlockVec d) : HCPolySupport.Book.Ch02.doubledMu U (Frozen.Section24.perturbCoeffOn U a h 0) P = HCPolySupport.Book.Ch02.doubledMu U a P

The doubled-mu value of the path at t = 0 is the base value.