Carrier

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

The public lower-tail sample carrier

The genuine lower-infinite cutoff is defined only on the full-measure carrier where every required lower shell tail converges. This module supplies that carrier and its canonical induced probability law; it deliberately does not define a cutoff value.

Main definitions

• Algsuperdiff.Section3.Cutoff.CutoffSample: the exact lower-tail-good subtype of the canonical shell-sequence carrier.
• Algsuperdiff.Section3.Cutoff.cutoffSampleLaw: the canonical shell law induced on that subtype.

@[reducible, inline]

abbrev Algsuperdiff.Section3.Cutoff.CutoffSample (d : ℕ) : Type

The public sample carrier for the genuine lower-infinite cutoff. Its elements are exactly the shell sequences satisfying LowerTailGood.

Equations

• Algsuperdiff.Section3.Cutoff.CutoffSample d = { omega : Algsuperdiff.Section3.Cutoff.ShellSeq d // Algsuperdiff.Section3.Cutoff.LowerTailGood omega }

theorem Algsuperdiff.Section3.Cutoff.ae_mem_range_cutoffSample_val {d : ℕ} (M : ABKModel d) : ∀ᵐ (omega : ShellSeq d) ∂↑M.P, omega ∈ Set.range Subtype.val

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffSampleLaw {d : ℕ} (M : ABKModel d) : MeasureTheory.ProbabilityMeasure (CutoffSample d)

The canonical probability law restricted to the exact lower-tail-good carrier.

Equations

• Algsuperdiff.Section3.Cutoff.cutoffSampleLaw M = ⟨MeasureTheory.Measure.comap Subtype.val ↑M.P, ⋯⟩

theorem Algsuperdiff.Section3.Cutoff.map_cutoffSampleLaw_val {d : ℕ} (M : ABKModel d) : MeasureTheory.Measure.map Subtype.val ↑(cutoffSampleLaw M) = ↑M.P

Pushing the induced cutoff-sample law forward along Subtype.val recovers the original canonical shell-sequence law.