BMatrix

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

The coarse matrix b as the pure-potential response

Source: ABK26 (e.big.Lambda.sensitivity). The descendant estimate of that display is stated for the one-cube matrix norm |b(R; a)|, while the sensitivity input is the response functional J. This module records the exact bridge between them.

The canonical coarse-matrix formula for the response (Ch02.responseJ_eq_coarseMatrices_formula_canonical) reads

J(U, p, q; a) = ½ p·σ p + ½ (q + κp)·σ_*^{-1}(q + κp) - p·q ,

so at the pure-potential loading q = 0 it collapses to

J(U, p, 0; a) = ½ p·(σ + κᵗ σ_*^{-1} κ) p = ½ p·b(U; a) p .

Since b is positive definite and symmetric, the one-cube norm |b| = coarseBMatrixNorm is exactly the supremum of that quadratic form over the unit sphere, which is the two-sided comparison proved below. The same formula applied to the transposed coefficient field shows that the pure-potential response is transpose-invariant; that is what removes the |p·q| shift from the adjoint budget of the descendant D_h estimate.

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

The pure-potential response is the b quadratic form

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.responseJ_potential_eq_half_bCoarse {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a p 0 = 1 / 2 * HCPolySupport.vecDot p (HCPolySupport.matVecMul (HCPolySupport.Book.Ch02.bCoarse U a) p)

2 J(U, p, 0; a) = p · b(U; a) p.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.responseJ_potential_transpose {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a.transpose p 0 = HCPolySupport.Book.Ch02.responseJ U a p 0

The pure-potential response is transpose invariant.

This is the exact reason why the adjoint half of the zero-trace witness carries no |p·q| shift at the pure-potential loading.

Two-sided comparison with the one-cube norm

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.two_mul_responseJ_potential_le_coarseBMatrixNorm {d : ℕ} (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (p : HCPolySupport.Vec d) : 2 * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (A.coeffOn Q) p 0 ≤ HCPolySupport.Book.Ch02.coarseBMatrixNorm Q A * HCPolySupport.vecNormSq p

The quadratic form of b never exceeds |b| |p|².

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.coarseBMatrixNorm_le_of_forall_responseJ_potential {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (p : HCPolySupport.Vec d), 2 * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (A.coeffOn Q) p 0 ≤ M * HCPolySupport.vecNormSq p) : HCPolySupport.Book.Ch02.coarseBMatrixNorm Q A ≤ M

A uniform quadratic-form bound gives the one-cube norm bound.