CoarseMatrixDerivativeCharacterization

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

theorem Algsuperdiff.Frozen.Section24.coarseMatrixDerivative_characterization {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : LInfMatrixFieldOn U) : HCPolySupport.IsSymmetricBlockMat (coarseMatrixDerivative U a h) ∧ (∀ (p q : HCPolySupport.Vec d) (vAdj : HCPolySupport.Book.Ch02.Solution U a.transpose) (v : HCPolySupport.Book.Ch02.Solution U a), HCPolySupport.Book.Ch02.IsResponseMaximizer U a.transpose p q vAdj → HCPolySupport.Book.Ch02.IsResponseMaximizer U a p (-q) v → HCPolySupport.blockVecDot (p, q) (HCPolySupport.blockMatVecMul (coarseMatrixDerivative U a h) (p, q)) = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (vAdj.toH1.grad x) (HCPolySupport.matVecMul (↑h x) (v.toH1.grad x))) ∧ ∀ (D : HCPolySupport.BlockMat d), HCPolySupport.IsSymmetricBlockMat D → (∀ (p q : HCPolySupport.Vec d) (vAdj : HCPolySupport.Book.Ch02.Solution U a.transpose) (v : HCPolySupport.Book.Ch02.Solution U a), HCPolySupport.Book.Ch02.IsResponseMaximizer U a.transpose p q vAdj → HCPolySupport.Book.Ch02.IsResponseMaximizer U a p (-q) v → HCPolySupport.blockVecDot (p, q) (HCPolySupport.blockMatVecMul D (p, q)) = HCPolySupport.Book.Ch02.average U fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (vAdj.toH1.grad x) (HCPolySupport.matVecMul (↑h x) (v.toH1.grad x))) → D = coarseMatrixDerivative U a h