G2Locality

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

The 𝒢₂ representative-level locality, via a.e. stability

The 𝒢₂ leg of the frozen good event is representative-based and choice-dependent on a null set: the public observable Support.annularErrorObservable is an A.mk of the (2,2) functional, so its values off one null set are an arbitrary measurable modification. Two consequences have to be discharged before the 𝒢₂ atoms can be fed to the independence producer:

1. Translation covariance must survive the choice. The manuscript's 𝓔_{s,2,2}(z+□_n; 𝐚_{n−2}, σ_{n−2}) is a literal object at a translated cube; the lane's atom is the representative at the origin read at the translated sample. These agree only a.e., and the null set moves with z.
2. Locality must survive the choice. cutoffSampleLocalSigma is the comap of a completed sigma-field, hence closed under a.e. modification; that is what makes the representative locally measurable at all, and it is the device this module exports at the function level.

Both are settled here, and the whole 𝒢₂ locality chain is then closed unconditionally.

The chain

Mu-locality (Section 3)
[measurable_Mu_coefficientCutoff_cutoffSampleLocal]
  → coarse full block matrix, literal                 [measurable_cutoffCoarseFullBlockRaw_local]
  → coarse full block matrix, representative          (a.e. stability)
  → normalized block response, representative         (continuous functional)
  → descendant average                                (finite average, subcubes stay inside)
  → the (2,2) functional at an ARBITRARY cube `Q`     [measurable_errorFunctionalAtCube_local]
  → the public 𝒢₂ observable read at the translated sample   (a.e. stability + covariance)
  → the annular maximum and the atom `X_j`

The coarse-block locality and a.e.-stability calculations use their common Section 3 producers, while this module supplies the representative-level and translated-observable applications.

The centres are lattice points

§4.1 centres are triadic lattice points z = 3^n v, so z + □_n is the triadic cube Localize.latticeCube n v. No translated-region sigma-field and no arbitrary-real-z locality is needed; the honest reading is the cube reading.

Scope

Provider material: proved local helpers.

References

• ABK26, d.good.event.for.lambda; l.ratio.of.good.scales.for.mathcal.E.

1. a.e. stability of the cutoff-sample local sigma-field

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_cutoffSampleLocalSigma_of_ae_eq {d : ℕ} {alpha : Type u_1} [MeasurableSpace alpha] (M : Section3.ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) {f g : Section3.Cutoff.CutoffSample d → alpha} (hf : Measurable f) (hfg : g =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] f) : Measurable g

The function-level a.e.-stability of cutoffSampleLocalSigma. The sigma-field is the Subtype.val-comap of a completed lower-shell local sigma-field, so a modification on a null set of a locally measurable map is locally measurable, in every codomain. This is the device that makes representative-based observables — the whole 𝒢₂ leg — usable at all.

2. The coarse-block chain

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_cutoffCoarseFullBlockRaw_local {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet Q ⊆ U) : Measurable (Section3.Observable.cutoffCoarseFullBlockRaw M L Q)

Every entry of the coarse block matrix of the actual cutoff on a cube is integral-local. CoarseGraining's four block-entry formulas express each entry through the coarse energy Mu, whose locality on the closed cube is proved.

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_cutoffCoarseFullBlockRepresentative_local {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet Q ⊆ U) : Measurable (Section3.Observable.cutoffCoarseFullBlockRepresentative M L Q)

The common coarse-block is local — the first genuine use of a.e. stability: the representative differs from the literal only on a null set.

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_cutoffNormalizedBlockResponseRepresentative_local {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) (a0 : HCPolySupport.Mat d) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet Q ⊆ U) : Measurable (Section3.Observable.cutoffNormalizedBlockResponseRepresentative M L Q a0)

The normalized block response of the common representative is local: it is a continuous finite-dimensional functional of the block matrix.

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_cutoffAvgDescendantNormalizedBlockResponseRepresentative_local {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a0 : HCPolySupport.Mat d) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet Q ⊆ U) : Measurable (Support.cutoffAvgDescendantNormalizedBlockResponseRepresentative M L Q k a0)

The descendant average is local: the subcubes of Q stay inside Q, hence inside the observation region.

3. The (2,2) functional at an arbitrary cube

noncomputable def Algsuperdiff.Section4.Provider.Proportion.errorFunctionalAtCube {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) : Section3.Cutoff.CutoffSample d → ℝ

The (2,2) measurable functional at an A triadic cube. At Q = □_n this is Support.cutoffHomogenizationError22Functional verbatim; the generality in Q is what carries the translated cubes z + □_n of the 𝒢₂ lane.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_errorFunctionalAtCube_local {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) {s : ℝ} (sigma : Section3.Observable.PositiveScalar) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet Q ⊆ U) : Measurable (errorFunctionalAtCube M L Q s sigma)

The (2,2) functional is local.

The functional IS the manuscript's literal, a.e.

theorem Algsuperdiff.Section4.Provider.Proportion.homogenizationErrorOnCube_two_two_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : 0 ≤ HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F a0

Nonnegativity of the literal (2,2) error at an arbitrary cube.

theorem Algsuperdiff.Section4.Provider.Proportion.errorFunctionalAtCube_eq_of_common_event {d : ℕ} (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (sigma : Section3.Observable.PositiveScalar) (omega : Section3.Cutoff.CutoffSample d) (hall : ∀ (R : HCPolySupport.TriadicCube d), HCPolySupport.Book.Ch02.normalizedBlockResponseMax R (Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) (Section3.Observable.isotropicComparatorMatrix sigma) = Section3.Observable.cutoffNormalizedBlockResponseRepresentative M L R (Section3.Observable.isotropicComparatorMatrix sigma) omega) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) (Section3.Observable.isotropicComparatorMatrix sigma) = errorFunctionalAtCube M L Q s sigma omega

On the probability-one event on which the literal block responses agree with their representatives triadic cube, the literal (2,2) error at Q equals the functional at Q.

theorem Algsuperdiff.Section4.Provider.Proportion.homogenizationErrorOnCube_two_two_ae_eq_errorFunctionalAtCube {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L : ℤ) (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (sigma : Section3.Observable.PositiveScalar) : (fun (omega : Section3.Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M L omega) (Section3.Observable.isotropicComparatorMatrix sigma)) =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] errorFunctionalAtCube M L Q s sigma

The literal (2,2) error at an arbitrary cube is a.e. the local functional.

4. The a.e. translation covariance of the public 𝒢₂ observable

theorem Algsuperdiff.Section4.Provider.Proportion.annularErrorObservable_comp_translate_ae_eq_literal {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (v : Fin d → ℤ) : (fun (omega : Section3.Cutoff.CutoffSample d) => Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n v) omega)) =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] fun (omega : Section3.Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (Localize.latticeCube n v) (↑s) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Cutoff.coefficientCutoffTriadicCoeffFamily M (n - 2) omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n - 2)))

The manuscript's literal event is recovered a.e. through the characterization lemmas, at the one place where that is load-bearing: the null set depends on v, and the identity is not pointwise.

theorem Algsuperdiff.Section4.Provider.Proportion.annularErrorObservable_comp_translate_ae_eq_functional {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (v : Fin d → ℤ) : (fun (omega : Section3.Cutoff.CutoffSample d) => Support.annularErrorObservable M n s (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint n v) omega)) =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] errorFunctionalAtCube M (n - 2) (Localize.latticeCube n v) (↑s) (Section3.Annealed.sigmaBar M (n - 2))

The public 𝒢₂ observable read at the translated sample is a.e. the local functional at the translated cube. Composing the atom bridge with the functional's a.e. identity.

5. Locality of the 𝒢₂ atom, the annular maximum, and X_j

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_errorAtomSq_local {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (v : Fin d → ℤ) {m : ℤ} (hm : n - 2 ≤ m) {U : Set (HCPolySupport.Vec d)} (hQU : HCPolySupport.cubeSet (Localize.latticeCube n v) ⊆ U) : Measurable (errorAtomSq M n s (Support.triadicLatticePoint n v))

The 𝒢₂ per-cube atom is local, at the truncation level n − 2 and every region containing the closed cube z + □_n = ⟨n, v⟩. This is the 𝒢₂ twin's translate-locality export, and the a.e.-stability step is where the representative choice is absorbed.

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_errorAnnMax_annulusRegion_local {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) {j n : ℤ} (hn : n ≤ j - 1) : Measurable (errorAnnMax M s j n)

The 𝒢₂ annular maximum is local on the annulus region of its own index: every read cube ⟨n, v⟩ with v in the annulus enumeration sits inside annulusRegion d j, and every truncation level n − 2 is at or below j − 2.

theorem Algsuperdiff.Section4.Provider.Proportion.measurable_Xcal_annulusRegion_local {d : ℕ} (M : Section3.ABKModel d) (s : { s : ℝ // 0 < s }) (j : ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => (XcalE M s j omega).toReal

X_j is local on annulusRegion d j at truncation level j − 2 — the hloc slot the independence producer consumes for the 𝒢₂ lane.