PointwiseExpansion

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

Pointwise second-difference expansion of the doubled coefficient matrix

The proof of l.sensitivity.coarse.grained.general rests on the pointwise algebra e.bfA.LDLt + e.Gh.additive: perturbing the coefficient matrix A by a skew matrix g conjugates the doubled matrix bfA by the shear G_{-g}, because the symmetric part is unchanged and the skew part is translated. At the level of quadratic forms this conjugation is exactly quadratic in the perturbation:

X · bfA(A + g) X = X · bfA(A) X - 2 (g X₁) · (bfA(A) X)₂ + (g X₁) · s⁻¹ (g X₁)

with s := symmPart A. This identity is pure matrix algebra: it never inverts s, so it holds for the Mathlib junk-value inverse as well. It is the entire second-difference content of the upper and lower coarse-matrix expansions; everything downstream is integration and minimizer bookkeeping.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.symmPart_add {d : ℕ} (A B : HCPolySupport.Mat d) : HCPolySupport.symmPart (A + B) = HCPolySupport.symmPart A + HCPolySupport.symmPart B

The symmetric part is additive.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.skewPart_add {d : ℕ} (A B : HCPolySupport.Mat d) : HCPolySupport.skewPart (A + B) = HCPolySupport.skewPart A + HCPolySupport.skewPart B

The skew part is additive.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.symmPart_smul {d : ℕ} (c : ℝ) (A : HCPolySupport.Mat d) : HCPolySupport.symmPart (c • A) = c • HCPolySupport.symmPart A

The symmetric part of a scalar multiple.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.skewPart_eq_self_of_symmPart_eq_zero {d : ℕ} {g : HCPolySupport.Mat d} (hg : HCPolySupport.symmPart g = 0) : HCPolySupport.skewPart g = g

A matrix with vanishing symmetric part is its own skew part.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.isSymm_symmPart {d : ℕ} (A : HCPolySupport.Mat d) : Matrix.IsSymm (HCPolySupport.symmPart A)

The symmetric part is a symmetric matrix.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.matTranspose_eq_neg_self_of_symmPart_eq_zero {d : ℕ} {g : HCPolySupport.Mat d} (hg : HCPolySupport.symmPart g = 0) : HCPolySupport.matTranspose g = -g

A matrix with vanishing symmetric part is antisymmetric.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecDot_matVecMul_self_eq_zero_of_symmPart_eq_zero {d : ℕ} {g : HCPolySupport.Mat d} (hg : HCPolySupport.symmPart g = 0) (ξ : HCPolySupport.Vec d) : HCPolySupport.vecDot ξ (HCPolySupport.matVecMul g ξ) = 0

The quadratic form of a matrix with vanishing symmetric part vanishes.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.vecDot_matVecMul_antisymm_of_symmPart_eq_zero {d : ℕ} {g : HCPolySupport.Mat d} (hg : HCPolySupport.symmPart g = 0) (u v : HCPolySupport.Vec d) : HCPolySupport.vecDot u (HCPolySupport.matVecMul g v) = -HCPolySupport.vecDot v (HCPolySupport.matVecMul g u)

The bilinear pairing of a matrix with vanishing symmetric part is antisymmetric.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockMatrixField_eq_blockMatrixOfCoeff {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (x : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.blockMatrixField a x = HCPolySupport.blockMatrixOfCoeff (a.toCoeffField x)

The Chapter 2 doubled matrix field is the pointwise doubled matrix of the coefficient representative.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockMatVecMul_blockMatrixOfCoeff_snd {d : ℕ} (A : HCPolySupport.Mat d) (X : HCPolySupport.BlockVec d) : (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X).2 = -HCPolySupport.matVecMul (HCPolySupport.symmPart A)⁻¹ (HCPolySupport.matVecMul (HCPolySupport.skewPart A) X.1 - X.2)

Second component of bfA(A) X, in the canonical s⁻¹ (k X₁ - X₂) form.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockMatVecMul_blockMatrixOfCoeff_fst {d : ℕ} (A : HCPolySupport.Mat d) (X : HCPolySupport.BlockVec d) : (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X).1 = HCPolySupport.matVecMul (HCPolySupport.symmPart A) X.1 + HCPolySupport.matVecMul (HCPolySupport.skewPart A) (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X).2

First component of bfA(A) X, expressed through the second component.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockQuadForm_blockMatrixOfCoeff {d : ℕ} (A : HCPolySupport.Mat d) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X) = HCPolySupport.vecDot X.1 (HCPolySupport.matVecMul (HCPolySupport.symmPart A) X.1) + HCPolySupport.vecDot (HCPolySupport.matVecMul (HCPolySupport.skewPart A) X.1 - X.2) (HCPolySupport.matVecMul (HCPolySupport.symmPart A)⁻¹ (HCPolySupport.matVecMul (HCPolySupport.skewPart A) X.1 - X.2))

The canonical form X·bfA(A)X = X₁·sX₁ + (kX₁ - X₂)·s⁻¹(kX₁ - X₂) of the doubled quadratic form. No invertibility of s is used.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockMatVecMul_blockMatrixOfCoeff_transpose_fluxFlip_snd {d : ℕ} (A : HCPolySupport.Mat d) (X : HCPolySupport.BlockVec d) : (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff (HCPolySupport.matTranspose A)) (X.1, -X.2)).2 = -(HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X).2

The second component of bfA X flips sign under simultaneous transpose of the coefficient matrix and flux flip of the doubled vector.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockQuadForm_transpose_fluxFlip {d : ℕ} (A : HCPolySupport.Mat d) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (X.1, -X.2) (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff (HCPolySupport.matTranspose A)) (X.1, -X.2)) = HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X)

The doubled quadratic form is invariant under simultaneous transpose of the coefficient matrix and flux flip of the doubled vector.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Path.blockQuadForm_add_skew {d : ℕ} (A : HCPolySupport.Mat d) {g : HCPolySupport.Mat d} (hg : HCPolySupport.symmPart g = 0) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff (A + g)) X) = HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X) - 2 * HCPolySupport.vecDot (HCPolySupport.matVecMul g X.1) (HCPolySupport.blockMatVecMul (HCPolySupport.blockMatrixOfCoeff A) X).2 + HCPolySupport.vecDot (HCPolySupport.matVecMul g X.1) (HCPolySupport.matVecMul (HCPolySupport.symmPart A)⁻¹ (HCPolySupport.matVecMul g X.1))

Exact pointwise second-difference expansion. For a skew perturbation g of the coefficient matrix A, the doubled quadratic form expands exactly: no remainder beyond the explicit quadratic term. This is the pointwise core of both the upper coarse-matrix expansion at the base field and (applied at the shifted base) the lower expansion.