TwoTermTranslation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Translation of two-term weak-Orlicz bounds #
This module transports a two-term weak-Orlicz bound along the measure-preserving translation action on cutoff samples. Both measurable witnesses are translated together, so their pointwise domination and their individual tail scales are unchanged.
Main result #
isTwoTermBigOWith_comp_translateCutoffSample: translation preserves anIsTwoTermBigOWithbound without changing either profile or amplitude.
theorem
Algsuperdiff.Section3.Provider.BadEvents.isTwoTermBigOWith_comp_translateCutoffSample
{d : ℕ}
(M : ABKModel d)
(z : HCPolySupport.Vec d)
{Ψ₁ Ψ₂ : ℝ → ℝ}
{X : Cutoff.CutoffSample d → ℝ}
{A₁ A₂ : ℝ}
(h : Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) Ψ₁ Ψ₂ X A₁ A₂)
:
Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) Ψ₁ Ψ₂
(fun (omega : Cutoff.CutoffSample d) => X (Cutoff.translateCutoffSample z omega)) A₁ A₂
A two-term weak-Orlicz bound on the cutoff carrier is preserved under every real translation of the sample, with the same two profiles and amplitudes.