ExistsUniqueCoarseMatrixDerivative

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

theorem Algsuperdiff.Frozen.Section24.existsUnique_coarseMatrixDerivative {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : LInfMatrixFieldOn U) : ∃! 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))