ScalarForcing

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

Bounds for a bounded scalar source

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.memScalarL2_of_memScalarLInfOn_of_subset {d : ℕ} {U W : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → ℝ} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict W)] (hWU : W ⊆ U) (hg : MemScalarLInfOn U g) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict W)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedL2On_le_scalarLInfSizeOn {d : ℕ} {U W : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → ℝ} (hWU : W ⊆ U) (hW : 0 < (MeasureTheory.volume W).toReal) (hg : MemScalarLInfOn U g) : Section4.Support.normalizedL2On W g ≤ scalarLInfSizeOn U g

A normalized L² average is bounded by the essential supremum.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.isMatrixDivFormWeakSolutionZerothOrderOn_restrict {d : ℕ} {a : HCPolySupport.CoeffField d} {W V : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hV : IsOpen V) (hVW : V ⊆ W) {u : HCPolySupport.H1Function W} {g : HCPolySupport.Vec d → ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : IsMatrixDivFormWeakSolutionZerothOrderOn a W u g f) : IsMatrixDivFormWeakSolutionZerothOrderOn a V (u.restrict hV hVW) g f

Restriction of the equation with a scalar zeroth-order source.