LawCarrier

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

Chapter 4 law carrier of the genuine coefficient cutoff

For every public lower-tail sample, the literal cutoff coefficient has the canonical compatible Chapter 2 coefficient family. This gives locally a.e. uniform ellipticity everywhere on the source carrier. The Chapter 4 RestrictionLawCarrier then follows by transport through the actual measurable pushforward law; no stationarity, range, isotropy, adjoint invariance, or quantitative input is bundled here.

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoff_aeeEllipticOn {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Book.Ch04.AEEllipticOn M.nu (coefficientCutoffCubeEllipticityUpper M m omega Q) (HCPolySupport.openCubeSet Q) (coefficientCutoff M.nu m omega)

On every triadic cube, the literal cutoff coefficient has the exact a.e. ellipticity data stored by its canonical Chapter 2 CoeffOn object.

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoff_aeLocallyUniformlyEllipticField {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : CutoffSample d) : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticField (coefficientCutoff M.nu m omega)

Every genuine cutoff realization belongs to the exact Chapter 4 local a.e.-uniform-ellipticity carrier. The witnesses are the source coefficient's canonical cube-wise CoeffOn witnesses, including their realised upper bound.

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_aeLocallyUniformlyElliptic {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.AELocallyUniformlyEllipticLaw (coefficientCutoffLaw M m)

The actual pushforward coefficient law is supported on the exact Chapter 4 locally a.e.-uniformly elliptic carrier.

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_lawCarrier {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionLawCarrier (coefficientCutoffLaw M m)

The genuine cutoff law supplies exactly the two Chapter 4 RestrictionLawCarrier fields: probability and local a.e.-uniform ellipticity support.