LocalizedAssembly

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

The localized quantities are measurable functions of the sample

The two localized quantities of Section 5.1 are suprema over the whole normalized forcing class, which is not countable, of quantities attached to almost-everywhere classes of Sobolev functions. They are nevertheless measurable, with no regularity hypothesis at all.

Both inner quantities are countable suprema of ball averages: the L^∞ norm of a difference by the essential-supremum identification, and the Hölder seminorm of the continuous representative by the identification that also reads ⊤ where no continuous representative exists. A ball average of the solution is a measurable function of the sample, and it is continuous in the forcing field — by the energy estimate, the zero-trace Poincaré inequality and Cauchy-Schwarz, none of which sees any regularity — so each inner quantity is lower semicontinuous in the datum and its supremum over the normalized class is attained on the countable subclass that approximates that class uniformly.

Main results

• measurable_localizedRegularity, measurable_localizedError — unconditional.
• measurable_percolationScaleTotal — the resulting measurability of the percolation scale.

References

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

1. The inner quantities as ball-average gauges

theorem Algsuperdiff.Section5.Support.integrableOn_h1Function {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} (u : HCPolySupport.H1Function (cubeSetAt y n)) : MeasureTheory.IntegrableOn u.toFun (cubeSetAt y n) MeasureTheory.volume

theorem Algsuperdiff.Section5.Support.iInf_isCubeRepresentative_eq_ballAverageHolderOn {d : ℕ} [NeZero d] {y : HCPolySupport.Vec d} {n : ℤ} {D : Set (HCPolySupport.Vec d)} (hD : Dense D) (u : HCPolySupport.H1Function (cubeSetAt y n)) {c : ENNReal} (hc : c ≠ 0) : ⨅ (uRep : HCPolySupport.Vec d → ℝ), ⨅ (_ : IsCubeRepresentative y n u uRep), c * holderSeminormOn (cubeSetAt y n) (1 / 2) uRep = c * ballAverageHolderOn (cubeSetAt y n) D u.toFun

The infimum over the continuous representatives is the ball-average Hölder gauge, including the value ⊤ where no continuous representative exists.

theorem Algsuperdiff.Section5.Support.eLpNorm_top_sub_eq_ballAverageSupNormOn {d : ℕ} [NeZero d] {y : HCPolySupport.Vec d} {n : ℤ} {D : Set (HCPolySupport.Vec d)} (hD : Dense D) (u v : HCPolySupport.H1Function (cubeSetAt y n)) : MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.toFun x - v.toFun x) ⊤ (MeasureTheory.volume.restrict (cubeSetAt y n)) = ballAverageSupNormOn (cubeSetAt y n) D fun (x : HCPolySupport.Vec d) => u.toFun x - v.toFun x

The L^∞ norm of the difference of two solutions is the ball-average supremum gauge.

2. The localized regularity

theorem Algsuperdiff.Section5.Support.measurable_localizedRegularity {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) : Measurable (localizedRegularity M n y)

The localized regularity is a measurable function of the sample.

3. The localized error

theorem Algsuperdiff.Section5.Support.measurable_localizedError {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) : Measurable (localizedError M n y)

The localized error is a measurable function of the sample.

4. The chain to the percolation scale

theorem Algsuperdiff.Section5.Support.measurable_percolationScaleTotal_of_model {d : ℕ} (M : Section3.ABKModel d) (Creg Cinj : ℝ) (m : ℤ) (ep : ℝ) : Measurable (percolationScaleTotal M Creg Cinj m ep)

The percolation scale is a measurable function of the sample, with no hypothesis beyond the model: the two localized quantities are measurable, hence so are the good cube event, the event Q, and the least scale beyond which no light crossing occurs.