ErrorRepresentative22

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

The measurable (2,2) homogenization-error representative

Algsuperdiff.Section4.Support.ErrorAtoms records the literal (2,2) observable cutoffHomogenizationErrorRaw22 and the 𝒢₂ atom annularErrorAtom. Neither is measurable by composition: CoarseGraining's normalizedBlockResponseMax is an sSup over the uncountable set of doubled unit directions. Section 3 solves this once and for all at (∞,2) in Observable/CutoffHomogenizationErrorRepresentative.lean: one measurable full coarse-block matrix is selected per cube, the compact-sphere norm functional is applied to it, and the countable scale sum is selected with A.mk with an explicit a.e. equality back to the literal.

This module is the (2,2) sibling of that construction. Three of its four layers are reused verbatim from the proved (∞,2) chain, because they are exponent-independent: the coarse-block representative (cutoffCoarseFullBlockRepresentative), its normalized response (cutoffNormalizedBlockResponseRepresentative), and the single probability-one event on which the literal maximum equals that response at every triadic cube (ae_forall_normalizedBlockResponseMax_cutoff_eq_representative).

Only the scale aggregation changes. At p = ∞ CoarseGraining's scaleResponseAtScale takes the descendant maximum (finsetSupReal); at p = 2 it takes the descendant average (finsetAverageReal) of the same normalized maxima, with the inner exponent p / 2 = 1. Consequently the squared identity homogenizationErrorOnCube_two_two_sq_eq_tsum below is the exact (2,2) sibling of CoarseGraining's Ch02.homogenizationErrorOnCube_infinity_two_sq_eq_tsum (Book/Ch02/Theorems/HomogenizationError/Finite.lean), and the finite average of finitely many genuinely measurable representatives is measurable with no Finset.sup' induction at all.

Main definitions

• cutoffAvgDescendantNormalizedBlockResponseRepresentative — the descendant average of the common coarse-block responses.
• cutoffHomogenizationErrorRepresentative22 — the genuine measurable nonnegative (2,2) representative.
• annularErrorObservable — the 𝒢₂ observable 𝓔_{s,2,2}(□_n; a_{n−2}, σ_{n−2} Id).

Main results

• homogenizationErrorOnCube_two_two_sq_eq_tsum — the (2,2) squared identity.
• cutoffHomogenizationErrorRaw22_ae_eq_representative22 — the semantic bridge.
• annularErrorAtom_ae_eq_annularErrorObservable — the same bridge at the 𝒢₂ atom.

References

• ABK26, d.good.event.for.lambda.

The (2,2) squared identity

theorem Algsuperdiff.Section4.Support.homogenizationErrorOnCube_two_two_sq_eq_tsum {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F a0 ^ 2 = ∑' (l : ℕ), HCPolySupport.Book.Ch02.geometricWeight s 2 l * HCPolySupport.Book.Ch02.finsetAverageReal (HCPolySupport.descendantsAtScale Q (Q.scale - ↑l)) fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F a0

The (2,2) sibling of CoarseGraining's Ch02.homogenizationErrorOnCube_infinity_two_sq_eq_tsum: after squaring, the q = 2 root disappears and 𝓔_{s,2,2} is exactly the geometrically weighted sum of the descendant averages of the normalized block-response maxima.

The descendant average of the common coarse-block responses

noncomputable def Algsuperdiff.Section4.Support.cutoffAvgDescendantNormalizedBlockResponseRepresentative {d : ℕ} (M : Section3.ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (k : ℤ) (a0 : HCPolySupport.Mat d) : Section3.Cutoff.CutoffSample d → ℝ

The finite descendant average formed from the canonical common-block representatives. This is the only layer where the (2,2) chain differs from the proved (∞,2) chain, which takes Ch02.finsetSupReal here.

Equations

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

theorem Algsuperdiff.Section4.Support.measurable_cutoffAvgDescendantNormalizedBlockResponseRepresentative {d : ℕ} (M : Section3.ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (k : ℤ) (a0 : HCPolySupport.Mat d) : Measurable (cutoffAvgDescendantNormalizedBlockResponseRepresentative M coefficientScale Q k a0)

The descendant average of genuinely measurable representatives is genuinely measurable: a finite sum needs no Finset.sup' induction and no a.e. qualification.

theorem Algsuperdiff.Section4.Support.cutoffAvgDescendantNormalizedBlockResponseRepresentative_nonneg {d : ℕ} (M : Section3.ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (k : ℤ) (a0 : HCPolySupport.Mat d) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ cutoffAvgDescendantNormalizedBlockResponseRepresentative M coefficientScale Q k a0 omega

The (2,2) functional and its measurable representative

noncomputable def Algsuperdiff.Section4.Support.cutoffHomogenizationError22Functional {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) : Section3.Cutoff.CutoffSample d → ℝ

The nonnegative everywhere-defined countable-sum functional of the (2,2) error, before selecting its measurable modification.

Equations

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

theorem Algsuperdiff.Section4.Support.cutoffHomogenizationError22Functional_nonneg {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ cutoffHomogenizationError22Functional M coefficientScale domainScale s sigma omega

theorem Algsuperdiff.Section4.Support.aemeasurable_cutoffHomogenizationError22Functional {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) : AEMeasurable (cutoffHomogenizationError22Functional M coefficientScale domainScale s sigma) ↑(Section3.Cutoff.cutoffSampleLaw M)

noncomputable def Algsuperdiff.Section4.Support.cutoffHomogenizationErrorRepresentative22 {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) : Section3.Cutoff.CutoffSample d → ℝ

The genuine measurable, nonnegative representative of the (2,2) cutoff homogenization error. The max 0 is not a fallback: it makes the canonical measurable modification nonnegative everywhere, while cutoffHomogenizationErrorRaw22_ae_eq_representative22 records its precise a.e. identity with the literal.

Equations

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

theorem Algsuperdiff.Section4.Support.measurable_cutoffHomogenizationErrorRepresentative22 {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) : Measurable (cutoffHomogenizationErrorRepresentative22 M coefficientScale domainScale s sigma)

theorem Algsuperdiff.Section4.Support.cutoffHomogenizationErrorRepresentative22_nonneg {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ cutoffHomogenizationErrorRepresentative22 M coefficientScale domainScale s sigma omega

theorem Algsuperdiff.Section4.Support.cutoffHomogenizationError22Functional_ae_eq_representative22 {d : ℕ} (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : Section3.Observable.PositiveScalar) : cutoffHomogenizationError22Functional M coefficientScale domainScale s sigma =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] cutoffHomogenizationErrorRepresentative22 M coefficientScale domainScale s sigma

theorem Algsuperdiff.Section4.Support.cutoffHomogenizationErrorRaw22_ae_eq_representative22 {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (coefficientScale domainScale : ℤ) {s : ℝ} (hs : 0 < s) (sigma : Section3.Observable.PositiveScalar) : cutoffHomogenizationErrorRaw22 M coefficientScale domainScale s sigma =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] cutoffHomogenizationErrorRepresentative22 M coefficientScale domainScale s sigma

The genuine measurable (2,2) representative is almost everywhere exactly the literal manuscript observable 𝓔_{s,2,2}(□_m; a_L, σ Id) under the actual cutoff law. This is the only semantic bridge consumers may use.

The public 𝒢₂ observable

theorem Algsuperdiff.Section4.Support.neZero_of_model_ErrorRepresentative22 {d : ℕ} (M : Section3.ABKModel d) : NeZero d

The paper-wide assumption 2 ≤ d, stored in the model, supplies the nonzero-dimension instance required by CoarseGraining's doubled-response A.

noncomputable def Algsuperdiff.Section4.Support.annularErrorObservable {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) : Section3.Cutoff.CutoffSample d → ℝ

The translated atom at z + □_n is annularErrorObservable M n s ∘ Cutoff.translateCutoffSample z (resolution A4).

Equations

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

theorem Algsuperdiff.Section4.Support.measurable_annularErrorObservable {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) : Measurable (annularErrorObservable M n s)

theorem Algsuperdiff.Section4.Support.annularErrorObservable_nonneg {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ annularErrorObservable M n s omega

theorem Algsuperdiff.Section4.Support.annularErrorAtom_ae_eq_annularErrorObservable {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : { s : ℝ // 0 < s }) : annularErrorAtom M n ↑s =ᵐ[↑(Section3.Cutoff.cutoffSampleLaw M)] annularErrorObservable M n s

The public 𝒢₂ observable is almost everywhere the literal 𝒢₂ atom of ErrorAtoms.