RelativeComparatorProbe #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Relative comparator probe #
This module isolates the deterministic comparator algebra needed by the finite-corridor mean consumer. It provides the shared relative-origin error transport and controls the actual same-cutoff starred fluctuation probe by the physical cutoff homogenization error. Consumers apply these results directly.
theorem
Algsuperdiff.Section3.Provider.Homogenization.relativeOrigin_homogenizationError_eq_cutoffError
{d : ℕ}
(M : ABKModel d)
(L : ℤ)
(s : ℝ)
(sigma : Observable.PositiveScalar)
(omega : Cutoff.CutoffSample d)
:
have c := ↑(Cutoff.cutoffRelativeNormalizationShift d);
have h := L + c;
let aPhys := Cutoff.coefficientCutoff M.nu L omega;
have haPhys := ⋯;
let aRel := HCPolySupport.dilateReg (-h) aPhys;
have haRel := ⋯;
have Frel := HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aRel haRel;
HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d (-c)) s
HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) Frel
(Observable.isotropicComparatorMatrix sigma) = Observable.cutoffHomogenizationErrorRaw M L L s sigma omega
Relative normalization preserves the physical cutoff error for any comparator scalar and smoothing exponent.
theorem
Algsuperdiff.Section3.Provider.Homogenization.fullBlockQuadratic_starredFluctuation_relativeOrigin_sq_le_error
{d : ℕ}
[NeZero d]
(M : ABKModel d)
(L : ℤ)
{s : ℝ}
(hs : 0 < s)
(omega : Cutoff.CutoffSample d)
(q : HCPolySupport.FullBlockVec d)
:
have c := ↑(Cutoff.cutoffRelativeNormalizationShift d);
have h := L + c;
have sigma := Annealed.sigmaBar M L;
have a0 := Observable.isotropicComparatorMatrix sigma;
have B := HCPolySupport.Book.Ch02.constantFullBlockMatrix a0;
have C0 := HCPolySupport.Book.Ch02.constantBlockMatrix a0;
have R := HCPolySupport.originCube d (-c);
have aRel := HCPolySupport.dilateReg (-h) (Cutoff.coefficientCutoff M.nu L omega);
HCPolySupport.Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic
(starredFluctuationMatrix B C0 (HCPolySupport.cubeSet R) aRel) q ^ 2 ≤ 6 * (q ⬝ᵥ q) ^ 2 * (Observable.cutoffHomogenizationErrorRaw M L L s sigma omega ^ 2 + Observable.cutoffHomogenizationErrorRaw M L L s sigma omega ^ 4)
The relative-origin starred comparator probe is controlled by the physical cutoff homogenization error at the same cutoff.