StepFiveBoundaryDelta #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The window average of ∇h, and its cap #
theorem
Algsuperdiff.Section4.Provider.Regularity.norm_volumeAverageVec_truncatedWindow_le_of_bound
{d : ℕ}
{m j : ℤ}
{z : HCPolySupport.Vec d}
(hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))
{gradh : HCPolySupport.Vec d → HCPolySupport.Vec d}
{K : ℝ}
(hK : 0 ≤ K)
(hint :
∀ (i : Fin d),
MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => gradh y i) (ExcessDecay.truncatedWindow z m j)
MeasureTheory.volume)
(hbd : ∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖gradh y‖ ≤ K)
:
The window average is capped by any pointwise bound on the domain cube.
‖(∇h)_W‖ ≤ K whenever ‖∇h‖ ≤ K pointwise on □_m ⊇ W. This is the |avg ∇h| ≤ ‖∇h‖_{L^∞} step the boundary chain uses, taken at the pointwise binder
rather than at an essential supremum.