CampanatoRepresentative

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

Identification of the small-contrast Campanato representative

Lebesgue differentiation identifies the dyadic Campanato limit with the raw Sobolev representative almost everywhere. Open sup-balls are used by the Campanato estimate and closed sup-balls by the Besicovitch Vitali family; their boundaries have zero Lebesgue measure.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastValueIndicator {d : ℕ} (u : HCPolySupport.H1Function (smallContrastUnitBall d)) : HCPolySupport.Vec d → ℝ

The Sobolev value extended by zero from the small-contrast unit ball.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastValueIndicator u = (Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBall d).indicator u.toFun

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastValueIndicator_of_mem {d : ℕ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastUnitBall d) : smallContrastValueIndicator u x = u.toFun x

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.integrable_smallContrastValueIndicator {d : ℕ} (u : HCPolySupport.H1Function (smallContrastUnitBall d)) : MeasureTheory.Integrable (smallContrastValueIndicator u) MeasureTheory.volume

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ae_tendsto_setAverage_smallContrastValueIndicator {d : ℕ} (u : HCPolySupport.H1Function (smallContrastUnitBall d)) : ∀ᵐ (x : HCPolySupport.Vec d), Filter.Tendsto (fun (r : ℝ) => ⨍ (y : HCPolySupport.Vec d) in Metric.closedBall x r, smallContrastValueIndicator u y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (smallContrastValueIndicator u x))

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volumeAverage_metricBall_eq_setAverage_closedBall {d : ℕ} [NeZero d] (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.volumeAverage (Metric.ball x r) f = ⨍ (y : HCPolySupport.Vec d) in Metric.closedBall x r, f y

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.tendsto_smallContrastDyadicRadius_zero {d : ℕ} [NeZero d] : Filter.Tendsto (smallContrastDyadicRadius (smallContrastCampanatoRadius d)) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.campanatoRepresentative_ae_eq {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hcamp : HasSmallContrastBallCampanatoBound alpha K u) : smallContrastCampanatoRepresentative u.toFun =ᵐ[MeasureTheory.volume.restrict (smallContrastBall d (1 / 2))] u.toFun

The Campanato representative is the Sobolev representative almost everywhere on the interior half-ball.