CutoffHomogenizationErrorRepresentative

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

Measurable cutoff homogenization-error representative

This module constructs the actual measurable provider for the literal manuscript observable \mathcal E_{s,\infty,2}(\square_m; a_L, \sigma\operatorname{Id}).

The construction has three deliberately separate layers:

• cutoffHomogenizationErrorRaw remains the literal CoarseGraining expression;
• one measurable full coarse-block matrix is selected for each cube, and the compact-sphere norm functional is applied to it;
• the countable geometric sum is selected with A.mk, with an explicit a.e. equality back to the literal expression.

The coefficient cutoff scale L and observed cube scale m are independent arguments throughout. In particular, no L = m specialization is hidden in this measurable realization.

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

The everywhere-defined normalized response functional of the common measurable full coarse-block representative. Off the physical event it is still a norm of a continuous finite-dimensional functional, not an arbitrary replacement.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffNormalizedBlockResponseRepresentative {d : ℕ} (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (a0 : HCPolySupport.Mat d) : Measurable (cutoffNormalizedBlockResponseRepresentative M coefficientScale Q a0)

theorem Algsuperdiff.Section3.Observable.cutoffNormalizedBlockResponseRepresentative_nonneg {d : ℕ} (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (a0 : HCPolySupport.Mat d) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffNormalizedBlockResponseRepresentative M coefficientScale Q a0 omega

theorem Algsuperdiff.Section3.Observable.ae_normalizedBlockResponseMax_cutoff_eq_representative {d : ℕ} [NeZero d] (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (a0 : HCPolySupport.Mat d) : (fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q (Cutoff.coefficientCutoffTriadicCoeffFamily M coefficientScale omega) a0) =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cutoffNormalizedBlockResponseRepresentative M coefficientScale Q a0

At every fixed cube, the canonical full-matrix representative realizes CoarseGraining's literal normalized response maximum almost everywhere.

theorem Algsuperdiff.Section3.Observable.ae_forall_normalizedBlockResponseMax_cutoff_eq_representative {d : ℕ} [NeZero d] (M : ABKModel d) (coefficientScale : ℤ) (a0 : HCPolySupport.Mat d) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (Q : HCPolySupport.TriadicCube d), HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q (Cutoff.coefficientCutoffTriadicCoeffFamily M coefficientScale omega) a0 = cutoffNormalizedBlockResponseRepresentative M coefficientScale Q a0 omega

A single probability-one event identifies the literal normalized maximum with its common-coarse-block realization on every triadic cube. This countable consolidation is what licenses the later countable scale sum.

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

The finite descendant maximum formed from the canonical common-block representatives.

Equations

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

theorem Algsuperdiff.Section3.Observable.aemeasurable_cutoffMaxDescendantNormalizedBlockResponseRepresentative {d : ℕ} (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (k : ℤ) (hk : k ≤ Q.scale) (a0 : HCPolySupport.Mat d) : AEMeasurable (cutoffMaxDescendantNormalizedBlockResponseRepresentative M coefficientScale Q k a0) ↑(Cutoff.cutoffSampleLaw M)

theorem Algsuperdiff.Section3.Observable.cutoffMaxDescendantNormalizedBlockResponseRepresentative_nonneg {d : ℕ} (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (k : ℤ) (a0 : HCPolySupport.Mat d) (omega : Cutoff.CutoffSample d) : 0 ≤ cutoffMaxDescendantNormalizedBlockResponseRepresentative M coefficientScale Q k a0 omega

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

The nonnegative everywhere-defined finite-dimensional/countable-sum functional before selecting its measurable modification.

Equations

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

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

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

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

The genuine measurable, nonnegative representative of the cutoff homogenization error. The max 0 is not a fallback: it makes the canonical measurable modification nonnegative everywhere, while the following theorem records its precise a.e. identity with the nonnegative raw functional.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffHomogenizationErrorRepresentative {d : ℕ} (M : ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : PositiveScalar) : Measurable (cutoffHomogenizationErrorRepresentative M coefficientScale domainScale s sigma)

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

theorem Algsuperdiff.Section3.Observable.cutoffHomogenizationErrorFunctional_ae_eq_representative {d : ℕ} (M : ABKModel d) (coefficientScale domainScale : ℤ) (s : ℝ) (sigma : PositiveScalar) : cutoffHomogenizationErrorFunctional M coefficientScale domainScale s sigma =ᵐ[↑(Cutoff.cutoffSampleLaw M)] cutoffHomogenizationErrorRepresentative M coefficientScale domainScale s sigma

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

The genuine measurable representative is almost everywhere exactly the literal manuscript observable \mathcal E_{s,\infty,2}(\square_m; a_L, \sigma\operatorname{Id}) under the actual cutoff law. This is the only semantic bridge consumers may use.