LambdaLocal

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

Integral-local measurability of the multiscale ellipticity of the actual cutoff

CoarseGraining's ambient observables Ch04.lambdaSqCoeffField / Ch04.LambdaSqCoeffField are defined by a global dichotomy: if h: A a, a condition quantified over every triadic cube of R^d (Homogenization/Book/Ch04/Law.lean). Read on an arbitrary coefficient field this destroys locality. On the actual cutoff samples it does not: every omega : CutoffSample d satisfies the dichotomy (Cutoff.coefficientCutoff_aeLocallyUniformlyEllipticField), so the branch is always the Ch02 branch and the observable reads only the descendant tree of its cube.

This module turns that observation into genuine measurability for the integral-local information of the cutoff sample space. Nothing is a.e.: the whole chain

Mu  ->  coarseBlockMatrix entries  ->  operator norms  ->  descendant maxima
    ->  weighted series           ->  lambda_{s,q}^{-1}, Lambda_{s,q}

is proved Cutoff.cutoffSampleLocalSigma M m U-measurable for every U containing the closed cube, by re-running CoarseGraining's own A Mu engine (measurable_Mu_comp_aeeSlice_of_measurable_entryTest) on the everywhere-valid slice cover of the cutoff samples. No CoarseGraining file is changed.

The only a.e. step is the very last one, and it is forced by the definition of badLoc: Provider/BadEvents/CubeEllipticity.lean totalizes the multiscale ellipticity observables through A.mk representatives, which are determined only up to a null set. measurableSet_cutoffSampleLocalSigma_of_ae_eq below shows that the cutoff-sample local sigma-field — a comap of the completed lower-shell local sigma-field — is closed under almost-everywhere modification, which is exactly what absorbs that step.

Main results

• measurable_Mu_coefficientCutoff_cutoffSampleLocal: genuine locality of the coarse-grained energy of the actual cutoff.
• measurable_cubeLowerEllipticityInvLiteral_cutoffSampleLocal, measurable_cubeUpperEllipticityLiteral_cutoffSampleLocal: genuine locality of the literal multiscale ellipticity observables of the actual cutoff.
• measurableSet_cutoffSampleLocalSigma_of_ae_eq: the cutoff-sample local sigma-field is closed under a.e. modification.
• measurableSet_badLoc_cutoffSampleLocal: e.Bloc.def at the cube Q is measurable for the integral-local information of any set containing the closed cube Q, at shell index Q.scale.

Range constants (disclosed)

The whole chain is stated for an arbitrary observation set U with cubeSet Q ⊆ U: the descendant tree of Q used by lambda_{s,q} and Lambda_{s,q} consists of cubes R ⊆ Q, so nothing outside the closed cube is ever read.

References

• ABK26, e.Bloc.def.
• ABK26, (2.22)--(2.23).

Genuine locality of the coarse-grained energy of the actual cutoff

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_Mu_coefficientCutoff_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) (P0 : HCPolySupport.BlockVec d) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Mu (HCPolySupport.cubeSet R) P0 (Cutoff.coefficientCutoff M.nu m omega).toFun

The coarse-grained energy of the actual cutoff is integral-local. The A quantitative slices of cubeSet R cover all cutoff samples, because every cutoff sample is a locally a.e.-uniformly elliptic field; each slice is LocalSigmaR (cubeSet R)-measurable and CoarseGraining's carrier Mu engine is measurable on it, so the genuine cover assembles with no null bookkeeping.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_coarseSigmaStarInv_apply_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) (i j : Fin d) : Measurable fun (omega : Cutoff.CutoffSample d) => (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) (Cutoff.coefficientCutoff M.nu m omega).toFun).lowerRight i j

Every entry of the lower-right coarse block sigma_*^{-1} of the actual cutoff is integral-local. This is CoarseGraining's finite polarization identity, run at genuine measurability.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_coarseB_apply_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) (i j : Fin d) : Measurable fun (omega : Cutoff.CutoffSample d) => (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) (Cutoff.coefficientCutoff M.nu m omega).toFun).upperLeft i j

Every entry of the upper-left coarse block b of the actual cutoff is integral-local.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_coarseSigmaStarInvNorm_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) (Cutoff.coefficientCutoff M.nu m omega).toFun).lowerRight

The L^2 operator norm of the lower-right coarse block is integral-local.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_coarseBNorm_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet R) (Cutoff.coefficientCutoff M.nu m omega).toFun).upperLeft

The L^2 operator norm of the upper-left coarse block is integral-local.

Descendant maxima and the weighted series

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_maxDescendantSigmaStarInv_cutoffSampleLocal {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) (n : ℕ) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale R (R.scale - ↑n) (Cutoff.coefficientCutoff M.nu m omega)

The descendant maximum of |sigma_*^{-1}| of the actual cutoff is integral-local: every descendant of R is a subcube of R.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_maxDescendantB_cutoffSampleLocal {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) (n : ℕ) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale R (R.scale - ↑n) (Cutoff.coefficientCutoff M.nu m omega)

The descendant maximum of |b| of the actual cutoff is integral-local.

The weighted descendant series

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_weightedSigmaSeries_cutoffSampleLocal {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Measurable fun (omega : Cutoff.CutoffSample d) => ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * (HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale R (R.scale - ↑n) (Cutoff.coefficientCutoff M.nu m omega)).rpow (q / 2)

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_weightedBSeries_cutoffSampleLocal {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Measurable fun (omega : Cutoff.CutoffSample d) => ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * (HCPolySupport.Book.Ch04.maxDescendantBMatrixNormCoeffFieldAtScale R (R.scale - ↑n) (Cutoff.coefficientCutoff M.nu m omega)).rpow (q / 2)

The multiscale ellipticity observables of the actual cutoff

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeLowerEllipticityInvLiteral_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeLowerEllipticityInvLiteral M R m s q)

The literal inverse lower multiscale ellipticity of the actual cutoff is integral-local. Everything the observable reads lives in the descendant tree of R, hence inside any U containing the closed cube.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_cubeUpperEllipticityLiteral_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hRU : HCPolySupport.cubeSet R ⊆ U) {s : ℝ} (hs : 0 < s) (q : CoarseEllipticityExponent) : Measurable (cubeUpperEllipticityLiteral M R m s q)

The literal upper multiscale ellipticity of the actual cutoff is integral-local.

Monotonicity and a.e. stability of the cutoff-sample local sigma-fields

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerShellLocalSigma_mono {d : ℕ} {m n : ℤ} (hmn : m ≤ n) {U V : Set (HCPolySupport.Vec d)} (hUV : U ⊆ V) : Cutoff.lowerShellLocalSigma m U ≤ Cutoff.lowerShellLocalSigma n V

The lower-shell local sigma-field is monotone in the shell index and in the observation region.

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerShellLocalCompletion_mono {d : ℕ} (M : ABKModel d) {m n : ℤ} (hmn : m ≤ n) {U V : Set (HCPolySupport.Vec d)} (hUV : U ⊆ V) : Cutoff.lowerShellLocalCompletion M m U ≤ Cutoff.lowerShellLocalCompletion M n V

The completed lower-shell local sigma-field is monotone in the shell index and in the observation region.

theorem Algsuperdiff.Section3.Provider.BadEvents.cutoffSampleLocalSigma_mono {d : ℕ} (M : ABKModel d) {m n : ℤ} (hmn : m ≤ n) {U V : Set (HCPolySupport.Vec d)} (hUV : U ⊆ V) : Cutoff.cutoffSampleLocalSigma M m U ≤ Cutoff.cutoffSampleLocalSigma M n V

The cutoff-sample local sigma-field is monotone in the shell index and in the observation region.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_cutoffSampleLocalSigma_of_ae_eq {d : ℕ} (M : ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) {s t : Set (Cutoff.CutoffSample d)} (ht : MeasurableSet t) (hst : s =ᵐ[↑(Cutoff.cutoffSampleLaw M)] t) : MeasurableSet s

The cutoff-sample local sigma-field is closed under almost-everywhere modification. It is the Subtype.val-comap of the completed lower-shell local sigma-field, and Subtype.val is injective with full-measure range, so an a.e. modification on the carrier is realized by an a.e. modification upstairs.

The local ellipticity bad event

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_badLoc_cutoffSampleLocal {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet Q ⊆ U) : MeasurableSet (badLoc M Q)

e.Bloc.def is integral-local. The local coarse-grained ellipticity failure of the cube Q is measurable for the integral-local information of any region containing the closed cube Q, at the shell index Q.scale. The only a.e. step is the passage from the A.mk representatives used by the definition of badLoc to the literal observables; the target sigma-field absorbs it.