LocalizedGaugeMeasurable

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

At a fixed forcing field the two ball-average gauges are measurable in the sample

For one forcing field the ball-average supremum norm and the ball-average 1/2-Hölder seminorm of the solution are suprema of countably many ball averages, by density, and each ball average is a measurable function of the sample. Both gauges are therefore measurable functions of the sample, and neither asks for a continuous representative.

The comparator enters the supremum norm as a fixed function: the comparator background does not depend on the sample, so only the rough-field solution varies.

Main results

• measurable_ballAverageHolderOn_solution, measurable_ballAverageSupNormOn_solution_sub — the ball-average gauges, which need no representative at all.

References

• ABK26, the localized error and regularity quantities of Section 5.1.

1. Countable suprema indexed by points

2. The ball-average gauges

theorem Algsuperdiff.Section5.Support.measurable_ballAverageHolderOn_solution {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) {D : Set (HCPolySupport.Vec d)} (hD : D.Countable) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => ballAverageHolderOn (cubeSetAt y n) D (solutionAt M m n y omega hg).toFun

The ball-average Hölder gauge of the solution is a measurable function of the sample. No continuous representative is involved.

theorem Algsuperdiff.Section5.Support.measurable_ballAverageSupNormOn_solution_sub {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hKg : 0 ≤ Kg) (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) {D : Set (HCPolySupport.Vec d)} (hD : D.Countable) (v : HCPolySupport.H1Function (cubeSetAt y n)) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => ballAverageSupNormOn (cubeSetAt y n) D fun (z : HCPolySupport.Vec d) => (solutionAt M m n y omega hg).toFun z - v.toFun z

The ball-average supremum gauge of the difference between the solution and a fixed function is a measurable function of the sample.