EquationRestriction

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

Restriction of the matrix-coefficient equation

The Schauder iteration solves a comparison problem on every inner ball. This is the zero-extension transport of the ambient weak equation to those balls; it is the matrix-valued analogue of the scalar Section 6 restriction lemma.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.setIntegral_vecDot_extendByZero {d : ℕ} {W V : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hV : IsOpen V) (hVW : V ⊆ W) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (phi : HCPolySupport.H10Function V) : ∫ (p : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (F p) ((phi.extendByZeroToOpenSuperset ⋯ hW hVW).grad p) = ∫ (p : HCPolySupport.Vec d) in V, HCPolySupport.vecDot (F p) (phi.grad p)

The zero extension of a test function pairs with a fixed vector field exactly as the original test function does.