CoarseMatrixDerivative

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

noncomputable def Algsuperdiff.Frozen.Section24.coarseMatrixDerivative {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : LInfMatrixFieldOn U) : HCPolySupport.BlockMat d

The unique block matrix representing the coarse response derivative.

Equations

• Algsuperdiff.Frozen.Section24.coarseMatrixDerivative U a h = Classical.choose ⋯