SkewCancellation

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

Pointwise skew cancellation for the D_h splitting identity

Source: ABK26 (proof of l.Dh.bound, e.sensitivity.basic.split), first step. The splitting of the D_h quadratic form begins with the purely algebraic observation that an antisymmetric matrix annihilates its own quadratic form, so that ⨍ ∇w* · h ∇w = ⨍ ∇(w* + w) · h ∇w.

This step involves no integration by parts: it is a pointwise algebraic cancellation under the integral, valid for the almost-everywhere antisymmetric carrier. The genuine weak integration by parts (which requires the response combination to lie in H¹₀) is kept strictly separate, in WeakIBP.lean.

This module proves:

• the finite-dimensional algebra (sum_entry_mul_eq_zero_of_symmPart_eq_zero, vecDot_matVecMul_self_eq_zero_of_symmPart_eq_zero);
• the almost-everywhere integrand cancellation (skew_pairing_integrand_ae_eq);
• the average-level cancellation at arbitrary response maximizers, stated on the frozen coarseMatrixDerivative quadratic form evaluated at (p, -q) (quadForm_coarseMatrixDerivative_eq_average_sum_pairing), which is the exact first step of e.sensitivity.basic.split for the frozen target coarseMatrixDerivative_bound.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.entry_eq_neg_of_symmPart_eq_zero {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.symmPart H = 0) (i j : Fin d) : H i j = -H j i

Entrywise antisymmetry from a vanishing symmetric part.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.sum_entry_mul_eq_zero_of_symmPart_eq_zero {d : ℕ} {H B : HCPolySupport.Mat d} (hH : HCPolySupport.symmPart H = 0) (hB : ∀ (i j : Fin d), B i j = B j i) : ∑ i : Fin d, ∑ j : Fin d, H i j * B i j = 0

A matrix with vanishing symmetric part annihilates every symmetric two-index array.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.vecDot_matVecMul_self_eq_zero_of_symmPart_eq_zero {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.symmPart H = 0) (g : HCPolySupport.Vec d) : HCPolySupport.vecDot g (HCPolySupport.matVecMul H g) = 0

The quadratic form of a matrix with vanishing symmetric part is zero.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.vecDot_add_matVecMul_eq_of_symmPart_eq_zero {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.symmPart H = 0) (f g : HCPolySupport.Vec d) : HCPolySupport.vecDot (f + g) (HCPolySupport.matVecMul H g) = HCPolySupport.vecDot f (HCPolySupport.matVecMul H g)

Adding the second factor to the first factor of the skew pairing does not change it: the pointwise skew-cancellation identity.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.skew_pairing_integrand_ae_eq {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (F G : HCPolySupport.Vec d → HCPolySupport.Vec d) : (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x) (HCPolySupport.matVecMul (↑↑h x) (G x))) =ᵐ[HCPolySupport.volumeMeasureOn U.carrier] fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x + G x) (HCPolySupport.matVecMul (↑↑h x) (G x))

Almost-everywhere integrand form of the skew cancellation for an a.e. antisymmetric L∞ matrix field.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.average_skew_pairing_eq_average_sum_pairing {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (F G : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x) (HCPolySupport.matVecMul (↑↑h x) (G x))) = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (F x + G x) (HCPolySupport.matVecMul (↑↑h x) (G x))

Average-level skew cancellation for the D_h integrand: the source display ⨍ ∇w* · h ∇w = ⨍ ∇(w* + w) · h ∇w, with no integration by parts.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.quadForm_coarseMatrixDerivative_eq_average_sum_pairing {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (p q : HCPolySupport.Vec d) (vAdj : HCPolySupport.Book.Ch02.Solution U a.transpose) (v : HCPolySupport.Book.Ch02.Solution U a) (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer U a.transpose p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer U a p q v) : HCPolySupport.blockVecDot (p, -q) (HCPolySupport.blockMatVecMul (Frozen.Section24.coarseMatrixDerivative U a ↑h) (p, -q)) = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (vAdj.toH1.grad x + v.toH1.grad x) (HCPolySupport.matVecMul (↑↑h x) (v.toH1.grad x))

Skew-cancellation step of e.sensitivity.basic.split. At arbitrary response maximizers vAdj (for (aᵗ, p, -q)) and v (for (a, p, q)), the frozen D_h quadratic form at (p, -q) equals the average of the pairing with the summed gradient ∇vAdj + ∇v against h ∇v. This is the pointwise algebraic cancellation; no integration by parts is used.