Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 35c8980d

View on Github →

feat(analysis/asymptotics/specific_asymptotics): Cesaro averaging preserves convergence (#13825)

Estimated changes

Modified src/analysis/asymptotics/specific_asymptotics.lean

added theorem asymptotics.is_o.sum_range

added theorem asymptotics.is_o_sum_range_of_tendsto_zero

added theorem filter.tendsto.cesaro

added theorem filter.tendsto.cesaro_smul