Project-declaredLean 4.32.0
Ae tendsto zero of distribution le
ae_tendsto_zero_of_distribution_le
Plain-language statement
Suppose that, for every error threshold and every measure tolerance , one can choose so that the set where exceeds has measure at most . Then converges to for almost every .
harmonic analysisFourier analysismeasure theory
Source project: Carleson formalization
Person-level attribution pending.