LocalizedLocality

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

The localized quantities read only the cube

The localized error and the localized regularity of y + □_n are built from the solutions of Dirichlet problems on that cube for the coefficient field at scale n. The equation sees the field only on the cube, so both quantities are functions of the restriction of the field to the closed cube, and that restriction is a local observable of the closed cube. This module makes both halves precise and concludes that the two quantities, and hence the good cube event, lie in the local information of y + □_n.

The first half is a change of parameter: replacing the coefficient field by the field extended from its restriction to the closed cube changes neither the set of solutions nor the value of either quantity, because the two fields agree on the cube.

The second half is lower semicontinuity in that parameter. Almost-everywhere uniqueness collapses the supremum over the solutions of the rough-field problem to the selected one, and the ball-average characterizations turn each remaining inner quantity into a supremum of averages of that solution over balls inside the cube. Each such average is continuous in the coefficient field, by the energy estimate and the zero-trace Poincaré inequality, so each inner quantity is a supremum of continuous functions and the two quantities are suprema of those over the whole normalized forcing class. A supremum of lower semicontinuous functions is lower semicontinuous, so no countable reduction of the forcing class is needed here.

The large-scale event, by contrast, reads every shell at or above n and is not an event of the cube; only the good cube event, and its intersection with any other local event, is stated as local.

Main definitions

• fieldLocalizedError, fieldLocalizedRegularity — the two quantities as functions of a continuous coefficient field on the closed cube.

References

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

1. The two quantities as functions of the coefficient field on the cube

noncomputable def Algsuperdiff.Section5.Support.fieldLocalizedError {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (A : ↑(ellipticCube M.nu y n)) : ENNReal

The localized error of a continuous coefficient field on the closed cube.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section5.Support.fieldLocalizedRegularity {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (A : ↑(ellipticCube M.nu y n)) : ENNReal

The localized regularity of a continuous coefficient field on the closed cube.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_cutoff_iff_extendCoeff {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {u : HCPolySupport.H1Function (cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} : IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu m omega).toCoeffField y n u g ↔ IsDirichletSolutionAt (extendCoeff y n (coefficientCutoffRestrict M.nu m (closedCubeAt y n) omega)) y n u g

The cutoff coefficient field and the field extended from its restriction to the closed cube define the same localized Dirichlet problem.

theorem Algsuperdiff.Section5.Support.localizedError_eq_fieldLocalizedError {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : localizedError M n y omega = fieldLocalizedError M n y ⟨coefficientCutoffRestrict M.nu n (closedCubeAt y n) omega, ⋯⟩

The localized error reads the sample only through the coefficient field on the closed cube.

theorem Algsuperdiff.Section5.Support.localizedRegularity_eq_fieldLocalizedRegularity {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : localizedRegularity M n y omega = fieldLocalizedRegularity M n y ⟨coefficientCutoffRestrict M.nu n (closedCubeAt y n) omega, ⋯⟩

The localized regularity reads the sample only through the coefficient field on the closed cube.

2. The ball-average gauges see only the almost-everywhere class

theorem Algsuperdiff.Section5.Support.ballAverageSupNormOn_congr_ae {d : ℕ} {U D : Set (HCPolySupport.Vec d)} {f h : HCPolySupport.Vec d → ℝ} (hae : f =ᵐ[MeasureTheory.volume.restrict U] h) : ballAverageSupNormOn U D f = ballAverageSupNormOn U D h

The ball-average supremum gauge depends only on the almost-everywhere class of its argument on the ambient set: every ball it reads lies in that set.

theorem Algsuperdiff.Section5.Support.ballAverageHolderOn_congr_ae {d : ℕ} {U D : Set (HCPolySupport.Vec d)} {f h : HCPolySupport.Vec d → ℝ} (hae : f =ᵐ[MeasureTheory.volume.restrict U] h) : ballAverageHolderOn U D f = ballAverageHolderOn U D h

The ball-average Hölder gauge depends only on the almost-everywhere class of its argument on the ambient set.

3. Collapsing the solution binder

theorem Algsuperdiff.Section5.Support.rpow_three_neg_half_nonneg (n : ℤ) : 0 ≤ Real.rpow 3 (-↑n / 2)

The normalization constant of the forcing class of y + □_n is nonnegative.

theorem Algsuperdiff.Section5.Support.fieldLocalizedRegularity_eq_iSup {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) {D : Set (HCPolySupport.Vec d)} (hD : Dense D) (A : ↑(ellipticCube M.nu y n)) : fieldLocalizedRegularity M n y A = ⨆ (g : HCPolySupport.Vec d → HCPolySupport.Vec d), ⨆ (hg : NormalizedForceAt y n g), ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) * Real.rpow 3 (-↑n / 2)) * ballAverageHolderOn (cubeSetAt y n) D (solutionOfField M y n ⋯ hg A).toFun

The solution binder of the localized regularity collapses. Two solutions of the same problem agree almost everywhere, and the gauge sees only that class, so the supremum over the solutions is the value at the selected one, read off its ball averages.

theorem Algsuperdiff.Section5.Support.fieldLocalizedError_eq_iSup {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) {D : Set (HCPolySupport.Vec d)} (hD : Dense D) (A : ↑(ellipticCube M.nu y n)) : fieldLocalizedError M n y A = ⨆ (g : HCPolySupport.Vec d → HCPolySupport.Vec d), ⨆ (hg : NormalizedForceAt y n g), ⨆ (v : HCPolySupport.H1Function (cubeSetAt y n)), ⨆ (_ : IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n v g), ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) * Real.rpow 3 (-↑n)) * ballAverageSupNormOn (cubeSetAt y n) D fun (x : HCPolySupport.Vec d) => (solutionOfField M y n ⋯ hg A).toFun x - v.toFun x

The rough-field solution binder of the localized error collapses. The comparator binder is kept: the comparator background does not depend on the coefficient field.

4. Lower semicontinuity in the coefficient field

theorem Algsuperdiff.Section5.Support.lowerSemicontinuous_fieldLocalizedRegularity {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) : LowerSemicontinuous (fieldLocalizedRegularity M n y)

The localized regularity is lower semicontinuous in the coefficient field on the cube.

theorem Algsuperdiff.Section5.Support.lowerSemicontinuous_fieldLocalizedError {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) : LowerSemicontinuous (fieldLocalizedError M n y)

The localized error is lower semicontinuous in the coefficient field on the cube.

5. The two quantities are local observables of the closed cube

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

The localized error of y + □_n is measurable for the local information of the closed cube y + □_n.

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

The localized regularity of y + □_n is measurable for the local information of the closed cube y + □_n.

6. The good cube event

theorem Algsuperdiff.Section5.Support.measurableSet_goodCubeEvent_local {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) (n : ℤ) (y : HCPolySupport.Vec d) (ep : ℝ) : MeasurableSet (goodCubeEvent M Creg n y ep)

The good cube event is a local event of the closed cube.

theorem Algsuperdiff.Section5.Support.measurableSet_goodCubeEvent_local_of_subset {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) (n m : ℤ) (y : HCPolySupport.Vec d) (ep : ℝ) (hnm : n ≤ m) {U : Set (HCPolySupport.Vec d)} (hU : closedCubeAt y n ⊆ U) : MeasurableSet (goodCubeEvent M Creg n y ep)

The good cube event is a local event of any region containing the closed cube, at any scale at least n.