ZerothOrderOneStep

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

One dyadic comparison with a bounded scalar source

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.oneStep_normalizedGradient_half_zerothOrder {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function (HCPolySupport.euclideanBall z r)} {g : HCPolySupport.Vec d → ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} {delta alpha : ℝ} (hmeas : Measurable a) (ha : CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall z r) a delta) (halpha0 : 0 < alpha) (halpha1 : alpha < 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ smallContrastThreshold d alpha) (hu : IsMatrixDivFormWeakSolutionZerothOrderOn a (HCPolySupport.euclideanBall z r) u g f) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall z r))) (hf : HCPolySupport.MemVectorL2 (HCPolySupport.euclideanBall z r) f) : vectorNormalizedL2On (HCPolySupport.euclideanBall z (r / 2)) u.grad ≤ (1 + 2 * delta * (1 / 2) ^ (-↑d / 2)) * vectorNormalizedL2On (HCPolySupport.euclideanBall z r) u.grad + 2 * (1 / 2) ^ (-↑d / 2) * vectorNormalizedL2On (HCPolySupport.euclideanBall z r) f + 4 * (1 / 2) ^ (-↑d / 2) * unitCubeDirichletPoincareExplicit d * ↑d * r * Section4.Support.normalizedL2On (HCPolySupport.euclideanBall z r) g

The half-ball one-step estimate with an additional scalar source.