Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-02 18:14 237b1ea5

View on Github →

feat(analysis/specific_limits): proof of harmonic series diverging and preliminaries (#3233) This PR is made of two parts :

A few new generic lemmas, mostly by @PatrickMassot , in order/filter/at_top_bot.lean and topology/algebra/ordered.lean
Definition of the harmonic series, basic lemmas about it, and proof of its divergence, in analysis/specific_limits.lean Zulip : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Harmonic.20Series.20Divergence/near/201651652

Estimated changes

Modified src/analysis/calculus/local_extr.lean

Modified src/analysis/specific_limits.lean

added theorem half_le_harmonic_double_sub_harmonic

added def harmonic_series

added theorem harmonic_tendsto_at_top

added theorem mono_harmonic

added theorem self_div_two_le_harmonic_two_pow

Modified src/order/filter/at_top_bot.lean

modified theorem filter.monotone.tendsto_at_top_finset

modified theorem filter.prod_at_top_at_top_eq

modified theorem filter.prod_map_at_top_eq

added theorem filter.tendsto_at_top_at_top_iff_of_monotone

added theorem filter.tendsto_at_top_at_top_of_monotone'

modified theorem filter.tendsto_at_top_at_top_of_monotone

modified theorem filter.tendsto_at_top_mono

added theorem filter.tendsto_at_top_of_monotone_of_filter

added theorem filter.tendsto_at_top_of_monotone_of_subseq

modified theorem filter.tendsto_finset_image_at_top_at_top

added theorem filter.unbounded_of_tendsto_at_top

Modified src/order/filter/bases.lean

Modified src/order/filter/basic.lean

modified theorem filter.filter_eq_bot_of_not_nonempty

added theorem filter.tendsto_bot

modified theorem filter.tendsto_congr'

added theorem filter.tendsto_of_not_nonempty

Modified src/topology/algebra/ordered.lean

added theorem tendsto_at_top_csupr

added theorem tendsto_at_top_supr

added theorem tendsto_of_monotone