Documentation

Atlas.TheoryOfProbability.code.AeCauchyFromKMI

noncomputable def KolmogorovThreeSeries.gAc (A c : ) :

Helper function used in the Kolmogorov three-series / a.s. Cauchy arguments: given a truncation level A > 0 and a centering constant c, gAc A c x equals x · 1_{|y| ≤ A}(x) - c, i.e. it truncates x to zero outside the interval [-A, A] and then subtracts c. This is the form used to construct the centered, truncated summands Y_n - E Y_n for which one applies Kolmogorov's maximal inequality.

Instances For