CutoffLawTransport

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

Transporting the stream Γ_σ estimates to the cutoff sample law

The proved stream estimates of Algsuperdiff.Section3.Provider.Stream are all stated under the canonical shell-sequence law M.P.toMeasure on ShellSeq d, while every consumer downstream of the genuine lower-infinite cutoff works under Cutoff.cutoffSampleLaw M on the lower-tail-good subtype Cutoff.CutoffSample d. This module supplies the transport between the two.

The bridge is the exact push-forward identity Cutoff.map_cutoffSampleLaw_val: the sample law pushes forward along the subtype inclusion to the shell law. Because that inclusion is a measurable embedding, the induced identity on preimages holds for every subset of ShellSeq d, measurable or not, so the transport of a weak-Orlicz tail bound needs no measurability or admissibility hypothesis at all: an upper-tail event of fun omega => X omega.1 is by definition the inclusion preimage of the corresponding upper-tail event of X.

Main results

• Algsuperdiff.Section3.Provider.Stream.measure_preimage_val_cutoffSampleLaw: the inclusion preimage identity for arbitrary subsets.
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_cutoffSampleLaw_comp_val: the generic one-sided transfer.
• Algsuperdiff.Section3.Provider.Stream.isBigOWith_cutoffSampleLaw_of_forall_eq_comp_val: the same transfer for a sample-level function that is only known to factor through the inclusion pointwise.
• The _cutoffLaw corollaries: each principal proved stream export restated verbatim under Cutoff.cutoffSampleLaw M, with omega.1 in place of omega.

References

• ABK26 (the transported displays; see the source citations on the proved exports themselves).

The sample inclusion as a mass-preserving embedding

theorem Algsuperdiff.Section3.Provider.Stream.measurableEmbedding_cutoffSample_val {d : ℕ} : MeasurableEmbedding Subtype.val

The inclusion of the lower-tail-good sample carrier into the shell-sequence carrier is a measurable embedding.

theorem Algsuperdiff.Section3.Provider.Stream.measure_preimage_val_cutoffSampleLaw {d : ℕ} (M : ABKModel d) (s : Set (Cutoff.ShellSeq d)) : ↑(Cutoff.cutoffSampleLaw M) (Subtype.val ⁻¹' s) = ↑M.P s

Every subset of the shell-sequence carrier -- measurable or not -- pulls back along the sample inclusion with exactly its original mass. This is the measurable-embedding strengthening of Cutoff.map_cutoffSampleLaw_val.

theorem Algsuperdiff.Section3.Provider.Stream.measureReal_preimage_val_cutoffSampleLaw {d : ℕ} (M : ABKModel d) (s : Set (Cutoff.ShellSeq d)) : (↑(Cutoff.cutoffSampleLaw M)).real (Subtype.val ⁻¹' s) = (↑M.P).real s

The real-valued form of measure_preimage_val_cutoffSampleLaw, which is the shape consumed by the weak-Orlicz tail calculus.

The generic transfers

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_cutoffSampleLaw_comp_val {d : ℕ} {M : ABKModel d} {Psi : ℝ → ℝ} {X : Cutoff.ShellSeq d → ℝ} {A : ℝ} (hX : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) Psi X A) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) Psi (fun (omega : Cutoff.CutoffSample d) => X ↑omega) A

Generic transfer of a one-sided weak-Orlicz tail bound from the canonical shell law to the cutoff sample law. No measurability of X and no admissibility of Ψ is needed: the upper-tail event of fun omega => X omega.1 is definitionally the inclusion preimage of the upper-tail event of X, and the inclusion preserves the mass of every subset.

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_cutoffSampleLaw_of_forall_eq_comp_val {d : ℕ} {M : ABKModel d} {Psi : ℝ → ℝ} {X : Cutoff.ShellSeq d → ℝ} {Y : Cutoff.CutoffSample d → ℝ} {A : ℝ} (hY : ∀ (omega : Cutoff.CutoffSample d), Y omega = X ↑omega) (hX : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) Psi X A) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) Psi Y A

The one-sided transfer for a function already phrased on the sample carrier, given only that it factors pointwise through the inclusion.

The small-cube L^∞ increment bounds on the cutoff law

theorem Algsuperdiff.Section3.Provider.Stream.isBigOWith_gammaSigma_translatedIncrementSupBound_cutoffLaw {d : ℕ} (M : ABKModel d) {n m : ℤ} (hnm : n < m) (z : HCPolySupport.Vec d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.CutoffSample d) => translatedIncrementSupBound z n m ↑omega) (streamLinftyConst d * min √M.gamma⁻¹ √(↑m - ↑n) * 3 ^ (M.gamma * ↑m))

isBigOWith_gammaSigma_translatedIncrementSupBound under the cutoff sample law: the small-cube bound on a translated cube, at the same amplitude.