Increasing compactly supported endpoint cutoffs

The cutoffs are continuous, take values in [0,1], and equal one eventually at any fixed endpoint. Their supports include both sides of zero.

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

noncomputable def BGW.StableTrees.prefixCutoff (n : ℕ) (x : ℝ) : ℝ

Continuous endpoint cutoffs increasing to one.

Equations

• BGW.StableTrees.prefixCutoff n x = max 0 (min 1 (↑n + 1 - |x|))

theorem BGW.StableTrees.continuous_prefixCutoff (n : ℕ) : Continuous (prefixCutoff n)

Continuity of the endpoint cutoff.

theorem BGW.StableTrees.prefixCutoff_mem_Icc (n : ℕ) (x : ℝ) : prefixCutoff n x ∈ Set.Icc 0 1

The cutoff lies between zero and one.

theorem BGW.StableTrees.hasCompactSupport_prefixCutoff (n : ℕ) : HasCompactSupport (prefixCutoff n)

The cutoff vanishes outside a bounded interval.

theorem BGW.StableTrees.monotone_prefixCutoff (x : ℝ) : Monotone fun (n : ℕ) => prefixCutoff n x

Monotonicity in the cutoff radius.

theorem BGW.StableTrees.eventually_prefixCutoff_eq_one (x : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, prefixCutoff n x = 1

Each endpoint eventually lies in the region where the cutoff is one.