Law

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

The actual coefficient-cutoff law

For a fixed scale, the law used by the annealed Section 3 objects is not an extra datum. It is the pushforward of the canonical probability law on the public lower-tail convergence carrier along the genuine coefficient cutoff a_m = nu I + k_m.

noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoffProbabilityLaw {d : ℕ} (M : ABKModel d) (m : ℤ) : MeasureTheory.ProbabilityMeasure (HCPolySupport.RegCoeffField d)

The actual probability law of the coefficient cutoff a_m. Both the source carrier and the coefficient map are genuine measurable objects, so this definition has no default-value or a.e.-map branch.

Equations

• Algsuperdiff.Section3.Cutoff.coefficientCutoffProbabilityLaw M m = (Algsuperdiff.Section3.Cutoff.cutoffSampleLaw M).map (Algsuperdiff.Section3.Cutoff.coefficientCutoff M.nu m)

noncomputable def Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw {d : ℕ} (M : ABKModel d) (m : ℤ) : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d

The actual Chapter 4 coefficient law of a_m, forgetting only the probability-measure packaging.

Equations

• Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw M m = ↑(Algsuperdiff.Section3.Cutoff.coefficientCutoffProbabilityLaw M m)

instance Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_isProbability {d : ℕ} (M : ABKModel d) (m : ℤ) : MeasureTheory.IsProbabilityMeasure (coefficientCutoffLaw M m)

The cutoff coefficient law is a probability measure because it is the measurable pushforward of the induced canonical cutoff-sample law.

@[simp]

theorem Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_eq_map {d : ℕ} (M : ABKModel d) (m : ℤ) : coefficientCutoffLaw M m = MeasureTheory.Measure.map (coefficientCutoff M.nu m) ↑(cutoffSampleLaw M)