BoundedField

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

Bounded perturbations for the coarse-matrix derivative

The source carrier is frozen in LInfMatrixFieldOn. This module records the two analytic consequences needed by the construction of D_h: an L∞ matrix field maps vector L² fields to vector L², and hence the exact displayed pairing in e.def.Dh is integrable for arbitrary solutions.

theorem Algsuperdiff.Section24.memVectorL2_matVecMul_of_lInfMatrixFieldOn {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (h : Frozen.Section24.LInfMatrixFieldOn U) {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 U.carrier f) : HCPolySupport.MemVectorL2 U.carrier fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul (↑h x) (f x)