CutoffResponseJCommonRepresentative

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

Scalar cutoff responses from the common coarse-block representative

Section 3.5 takes a maximum over the uncountable Euclidean unit sphere. A separately chosen measurable modification for each direction cannot justify a single almost-sure event for that maximum. This module instead evaluates the one measurable representative of the entire coarse block matrix constructed in CutoffCoarseBlockRepresentative.

The scalar response is recovered as twice a doubled block response whose second scalar-response channel has zero loads. Since the full-block bridge is simultaneous in all doubled loads, the final almost-everywhere theorem has its quantifiers over every positive comparator and every direction inside one event.

References

• ABK26, (2.4), definition of J(U,p,q;a).
• ABK26, Section 3.5, Proposition p.homogenization.step.

noncomputable def Algsuperdiff.Section3.Observable.responseJFirstHalfBlockLoad {d : ℕ} (p q : HCPolySupport.Vec d) : HCPolySupport.BlockVec d

The first doubled load which isolates the scalar response with loads p,q.

Equations

• Algsuperdiff.Section3.Observable.responseJFirstHalfBlockLoad p q = ((1 / 2) • p, (-1 / 2) • q)

noncomputable def Algsuperdiff.Section3.Observable.responseJSecondHalfBlockLoad {d : ℕ} (p q : HCPolySupport.Vec d) : HCPolySupport.BlockVec d

The second doubled load which isolates the scalar response with loads p,q.

Equations

• Algsuperdiff.Section3.Observable.responseJSecondHalfBlockLoad p q = ((1 / 2) • q, (-1 / 2) • p)

noncomputable def Algsuperdiff.Section3.Observable.cutoffResponseJFromCommonCoarseBlock {d : ℕ} (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) : Cutoff.CutoffSample d → ℝ

Evaluate the scalar response with arbitrary loads p,q from the one common full coarse-block representative.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffResponseJFromCommonCoarseBlock {d : ℕ} (M : ABKModel d) (coefficientScale : ℤ) (Q : HCPolySupport.TriadicCube d) (p q : HCPolySupport.Vec d) : Measurable (cutoffResponseJFromCommonCoarseBlock M coefficientScale Q p q)

Fixed-load scalar evaluation of the common coarse-block representative is measurable.

noncomputable def Algsuperdiff.Section3.Observable.cutoffResponseJWithComparatorFromCommonCoarseBlock {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) (sigma : PositiveScalar) (e : HCPolySupport.Vec d) : Cutoff.CutoffSample d → ℝ

The Section 3.5 comparator specialization of the scalar evaluation from the common full coarse-block representative. Its cube and coefficient scales remain distinct: the cube is square_cubeScale, while the coefficient is the genuine cutoff a_coefficientScale.

Equations

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

theorem Algsuperdiff.Section3.Observable.measurable_cutoffResponseJWithComparatorFromCommonCoarseBlock {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) (sigma : PositiveScalar) (e : HCPolySupport.Vec d) : Measurable (cutoffResponseJWithComparatorFromCommonCoarseBlock M cubeScale coefficientScale sigma e)

For a fixed comparator and direction, evaluation of the common coarse block is measurable.

theorem Algsuperdiff.Section3.Observable.ae_forall_cutoffResponseJWithComparator_eq_fromCommonCoarseBlock {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (sigma : PositiveScalar) (e : HCPolySupport.Vec d), cutoffResponseJWithComparator M cubeScale coefficientScale sigma e omega = cutoffResponseJWithComparatorFromCommonCoarseBlock M cubeScale coefficientScale sigma e omega

One common probability-one event identifies the literal cutoff response with evaluation of the single full coarse-block representative for every positive comparator and every direction. In particular, no intersection of direction-indexed null sets is used.