feat(analysis/specific_limits): proof of harmonic series diverging an…

…d 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

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/calculus/local_extr.lean

@@ -121,7 +121,7 @@ lemma is_local_max_on.has_fderiv_within_at_nonpos {s : set E} (h : is_local_max_
 begin
   rcases hy with ⟨c, d, hd, hc, hcd⟩,
   have hc' : tendsto (λ n, ∥c n∥) at_top at_top,
-    from tendsto_at_top_mono _ (λ n, le_abs_self _) hc,
+    from tendsto_at_top_mono (λ n, le_abs_self _) hc,
   refine le_of_tendsto at_top_ne_bot (hf.lim at_top hd hc' hcd) _,
   replace hd : tendsto (λ n, a + d n) at_top (nhds_within (a + 0) s),
   from tendsto_inf.2 ⟨tendsto_const_nhds.add (tangent_cone_at.lim_zero _ hc' hcd),

src/analysis/specific_limits.lean

@@ -150,8 +150,8 @@ suffices tendsto (λ n : ℕ, 1 / (↑(n + 1) : ℝ)) at_top (𝓝 0), by simpa,
 lemma tendsto_add_one_pow_at_top_at_top_of_pos [linear_ordered_semiring α] [archimedean α] {r : α}
   (h : 0 < r) :
   tendsto (λ n:ℕ, (r + 1)^n) at_top at_top :=
-(tendsto_at_top_at_top_of_monotone (λ n m, pow_le_pow (le_add_of_nonneg_left' (le_of_lt h)))).2 $
-  λ x, (add_one_pow_unbounded_of_pos x h).imp $ λ _, le_of_lt
+tendsto_at_top_at_top_of_monotone' (λ n m, pow_le_pow (le_add_of_nonneg_left' (le_of_lt h))) $
+  not_bdd_above_iff.2 $ λ x, set.exists_range_iff.2 $ add_one_pow_unbounded_of_pos _ h
 
 lemma tendsto_pow_at_top_at_top_of_one_lt [linear_ordered_ring α] [archimedean α]
   {r : α} (h : 1 < r) :
@@ -586,3 +586,72 @@ begin
 end
 
 end ennreal
+
+/-!
+### Harmonic series
+
+Here we define the harmonic series and prove some basic lemmas about it,
+leading to a proof of its divergence to +∞ -/
+
+/-- The harmonic series `1 + 1/2 + 1/3 + ... + 1/n`-/
+def harmonic_series (n : ℕ) : ℝ :=
+∑ i in range n, 1/(i+1 : ℝ)
+
+lemma mono_harmonic : monotone harmonic_series :=
+begin
+  intros p q hpq,
+  apply sum_le_sum_of_subset_of_nonneg,
+  rwa range_subset,
+  intros x h _,
+  exact le_of_lt nat.one_div_pos_of_nat,
+end
+
+lemma half_le_harmonic_double_sub_harmonic (n : ℕ) (hn : 0 < n) :
+  1/2 ≤ harmonic_series (2*n) - harmonic_series n :=
+begin
+  suffices : harmonic_series n + 1 / 2 ≤ harmonic_series (n + n),
+  { rw two_mul,
+    linarith },
+  have : harmonic_series n + ∑ k in Ico n (n + n), 1/(k + 1 : ℝ) = harmonic_series (n + n) :=
+    sum_range_add_sum_Ico _ (show n ≤ n+n, by linarith),
+  rw [← this,  add_le_add_iff_left],
+  have : ∑ k in Ico n (n + n), 1/(n+n : ℝ) = 1/2,
+  { have : (n : ℝ) + n ≠ 0,
+    { norm_cast, linarith },
+    rw [sum_const, Ico.card],
+    field_simp [this],
+    ring },
+  rw ← this,
+  apply sum_le_sum,
+  intros x hx,
+  rw one_div_le_one_div,
+  { exact_mod_cast nat.succ_le_of_lt (Ico.mem.mp hx).2 },
+  { norm_cast, linarith },
+  { exact_mod_cast nat.zero_lt_succ x }
+end
+
+lemma self_div_two_le_harmonic_two_pow (n : ℕ) : (n / 2 : ℝ) ≤ harmonic_series (2^n) :=
+begin
+  induction n with n hn,
+  unfold harmonic_series,
+  simp only [one_div_eq_inv, nat.cast_zero, euclidean_domain.zero_div, nat.cast_succ, sum_singleton,
+    inv_one, zero_add, nat.pow_zero, range_one, zero_le_one],
+  have : harmonic_series (2^n) + 1 / 2 ≤ harmonic_series (2^(n+1)),
+  { have := half_le_harmonic_double_sub_harmonic (2^n) (by {apply nat.pow_pos, linarith}),
+    rw [nat.mul_comm, ← nat.pow_succ] at this,
+    linarith },
+  apply le_trans _ this,
+  rw (show (n.succ / 2 : ℝ) = (n/2 : ℝ) + (1/2), by field_simp),
+  linarith,
+end
+
+/-- The harmonic series diverges to +∞ -/
+theorem harmonic_tendsto_at_top : tendsto harmonic_series at_top at_top :=
+begin
+  suffices : tendsto (λ n : ℕ, harmonic_series (2^n)) at_top at_top, by
+  { exact tendsto_at_top_of_monotone_of_subseq mono_harmonic at_top_ne_bot this },
+  apply tendsto_at_top_mono self_div_two_le_harmonic_two_pow,
+  apply tendsto_at_top_div,
+  norm_num,
+  exact tendsto_coe_nat_real_at_top_at_top
+end

src/order/filter/at_top_bot.lean

@@ -109,14 +109,14 @@ lemma tendsto_at_top [preorder β] (m : α → β) (f : filter α) :
 by simp only [at_top, tendsto_infi, tendsto_principal]; refl
 
 lemma tendsto_at_top_mono' [preorder β] (l : filter α) ⦃f₁ f₂ : α → β⦄
-  (h : {x | f₁ x ≤ f₂ x} ∈ l) :
+  (h : ∀ᶠ x in l, f₁ x ≤ f₂ x) :
   tendsto f₁ l at_top → tendsto f₂ l at_top :=
 assume h₁, (tendsto_at_top _ _).2 $ λ b, mp_sets ((tendsto_at_top _ _).1 h₁ b)
   (monotone_mem_sets (λ a ha ha₁, le_trans ha₁ ha) h)
 
-lemma tendsto_at_top_mono [preorder β] (l : filter α) :
-  monotone (λ f : α → β, tendsto f l at_top) :=
-λ f₁ f₂ h, tendsto_at_top_mono' l $ univ_mem_sets' h
+lemma tendsto_at_top_mono [preorder β] {l : filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) :
+  tendsto f l at_top → tendsto g l at_top :=
+tendsto_at_top_mono' l $ eventually_of_forall _ h
 
 /-!
 ### Sequences
@@ -220,11 +220,11 @@ let ⟨φ, h, h'⟩ := extraction_of_frequently_at_top (frequently_high_scores h
 
 lemma strict_mono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ n, n ≤ u n) :
   ∃ φ : ℕ → ℕ, strict_mono φ ∧ strict_mono (u ∘ φ) :=
-strict_mono_subseq_of_tendsto_at_top (tendsto_at_top_mono _ hu tendsto_id)
+strict_mono_subseq_of_tendsto_at_top (tendsto_at_top_mono hu tendsto_id)
 
 lemma strict_mono_tendsto_at_top {φ : ℕ → ℕ} (h : strict_mono φ) :
   tendsto φ at_top at_top :=
-tendsto_at_top_mono _ h.id_le tendsto_id
+tendsto_at_top_mono h.id_le tendsto_id
 
 section ordered_add_monoid
 
@@ -346,48 +346,66 @@ lemma tendsto_at_top_at_bot [nonempty α] [decidable_linear_order α] [preorder
   tendsto f at_top at_bot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≥ f a :=
 @tendsto_at_top_at_top α (order_dual β) _ _ _ f
 
-lemma tendsto_at_top_at_top_of_monotone [nonempty α] [semilattice_sup α] [preorder β]
+lemma tendsto_at_top_at_top_of_monotone [preorder α] [preorder β] {f : α → β} (hf : monotone f)
+  (h : ∀ b, ∃ a, b ≤ f a) :
+  tendsto f at_top at_top :=
+tendsto_infi.2 $ λ b, tendsto_principal.2 $ let ⟨a, ha⟩ := h b in
+mem_sets_of_superset (mem_at_top a) $ λ a' ha', le_trans ha (hf ha')
+
+lemma tendsto_at_top_at_top_iff_of_monotone [nonempty α] [semilattice_sup α] [preorder β]
   {f : α → β} (hf : monotone f) :
   tendsto f at_top at_top ↔ ∀ b : β, ∃ a : α, b ≤ f a :=
 (tendsto_at_top_at_top f).trans $ forall_congr $ λ b, exists_congr $ λ a,
   ⟨λ h, h a (le_refl a), λ h a' ha', le_trans h $ hf ha'⟩
 
 alias tendsto_at_top_at_top_of_monotone ← monotone.tendsto_at_top_at_top
+alias tendsto_at_top_at_top_iff_of_monotone ← monotone.tendsto_at_top_at_top_iff
 
 lemma tendsto_finset_range : tendsto finset.range at_top at_top :=
-finset.range_mono.tendsto_at_top_at_top.2 finset.exists_nat_subset_range
+finset.range_mono.tendsto_at_top_at_top finset.exists_nat_subset_range
 
-lemma monotone.tendsto_at_top_finset [nonempty β] [semilattice_sup β]
+/-- If `f` is a monotone sequence of `finset`s and each `x` belongs to one of `f n`, then
+`tendsto f at_top at_top`. -/
+lemma monotone.tendsto_at_top_finset [semilattice_sup β]
   {f : β → finset α} (h : monotone f) (h' : ∀ x : α, ∃ n, x ∈ f n) :
   tendsto f at_top at_top :=
 begin
-  classical,
-  apply (tendsto_at_top_at_top_of_monotone h).2,
-  choose N hN using h',
-  assume b,
-  have : bdd_above ↑(b.image N) := finset.bdd_above _,
-  rcases this with ⟨n, hn⟩,
-  refine ⟨n, _⟩,
-  assume i ib,
-  have : N i ∈ ↑(finset.image N b),
-    by { rw finset.mem_coe, exact finset.mem_image_of_mem _ ib },
-  exact (h (hn this)) (hN i)
+  by_cases ne : nonempty β,
+  { resetI,
+    apply h.tendsto_at_top_at_top,
+    choose N hN using h',
+    assume b,
+    rcases (b.image N).bdd_above with ⟨n, hn⟩,
+    refine ⟨n, λ i ib, _⟩,
+    have : N i ∈ b.image N := finset.mem_image_of_mem _ ib,
+    exact h (hn $ finset.mem_coe.2 this) (hN i) },
+  { exact tendsto_of_not_nonempty ne }
 end
 
-lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : ∀x, j (i x) = x) :
+lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : function.left_inverse j i) :
   tendsto (finset.image j) at_top at_top :=
-have j ∘ i = id, from funext h,
-(finset.image_mono j).tendsto_at_top_at_top.2 $ assume s,
-  ⟨s.image i, by simp only [finset.image_image, this, finset.image_id, le_refl]⟩
-
-lemma prod_at_top_at_top_eq {β₁ β₂ : Type*} [nonempty β₁] [nonempty β₂] [semilattice_sup β₁]
-  [semilattice_sup β₂] : (@at_top β₁ _) ×ᶠ (@at_top β₂ _) = @at_top (β₁ × β₂) _ :=
-by inhabit β₁; inhabit β₂;
-  simp [at_top, prod_infi_left (default β₁), prod_infi_right (default β₂), infi_prod];
-    exact infi_comm
-
-lemma prod_map_at_top_eq {α₁ α₂ β₁ β₂ : Type*} [nonempty β₁] [nonempty β₂]
-  [semilattice_sup β₁] [semilattice_sup β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
+(finset.image_mono j).tendsto_at_top_at_top $ assume s,
+  ⟨s.image i, by simp only [finset.image_image, h.comp_eq_id, finset.image_id, le_refl]⟩
+
+lemma prod_at_top_at_top_eq {β₁ β₂ : Type*} [semilattice_sup β₁] [semilattice_sup β₂] :
+  (at_top : filter β₁) ×ᶠ (at_top : filter β₂) = (at_top : filter (β₁ × β₂)) :=
+begin
+  by_cases ne : nonempty β₁ ∧ nonempty β₂,
+  { cases ne,
+    resetI,
+    inhabit β₁,
+    inhabit β₂,
+    simp [at_top, prod_infi_left (default β₁), prod_infi_right (default β₂), infi_prod],
+    exact infi_comm },
+  { push_neg at ne,
+    cases ne;
+    { have : ¬ (nonempty (β₁ × β₂)), by simp [ne],
+      rw [at_top.filter_eq_bot_of_not_nonempty ne, at_top.filter_eq_bot_of_not_nonempty this],
+      simp only [bot_prod, prod_bot] } }
+end
+
+lemma prod_map_at_top_eq {α₁ α₂ β₁ β₂ : Type*} [semilattice_sup β₁] [semilattice_sup β₂]
+  (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
   (map u₁ at_top) ×ᶠ (map u₂ at_top) = map (prod.map u₁ u₂) at_top :=
 by rw [prod_map_map_eq, prod_at_top_at_top_eq, prod.map_def]
 
@@ -449,4 +467,41 @@ map_at_top_eq_of_gc (λb, b * k + (k - 1)) 1
       ... ≤ (b * k + (k - 1)) / k : nat.div_le_div_right $ nat.le_add_right _ _)
 
 
+/-- If `u` is a monotone function with linear ordered codomain and the range of `u` is not bounded
+above, then `tendsto u at_top at_top`. -/
+lemma tendsto_at_top_at_top_of_monotone' {ι α : Type*} [preorder ι] [linear_order α]
+  {u : ι → α} (h : monotone u) (H : ¬bdd_above (range u)) :
+  tendsto u at_top at_top :=
+begin
+  apply h.tendsto_at_top_at_top,
+  intro b,
+  rcases not_bdd_above_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩,
+  exact ⟨N, le_of_lt hN⟩,
+end
+
+lemma unbounded_of_tendsto_at_top {α β : Type*} [nonempty α] [semilattice_sup α]
+  [preorder β] [no_top_order β] {f : α → β} (h : tendsto f at_top at_top) :
+  ¬ bdd_above (range f) :=
+begin
+  rintros ⟨M, hM⟩,
+  cases mem_at_top_sets.mp (h $ Ioi_mem_at_top M) with a ha,
+  apply lt_irrefl M,
+  calc
+  M < f a : ha a (le_refl _)
+  ... ≤ M : hM (set.mem_range_self a)
+end
+
+/-- If a monotone function `u : ι → α` tends to `at_top` along *some* non-trivial filter `l`, then
+it tends to `at_top` along `at_top`. -/
+lemma tendsto_at_top_of_monotone_of_filter {ι α : Type*} [preorder ι] [preorder α] {l : filter ι}
+  {u : ι → α} (h : monotone u) (hl : l ≠ ⊥) (hu : tendsto u l at_top) :
+  tendsto u at_top at_top :=
+h.tendsto_at_top_at_top $ λ b, (hu.eventually (mem_at_top b)).exists hl
+
+lemma tendsto_at_top_of_monotone_of_subseq {ι ι' α : Type*} [preorder ι] [preorder α] {u : ι → α}
+  {φ : ι' → ι} (h : monotone u) {l : filter ι'} (hl : l ≠ ⊥)
+  (H : tendsto (u ∘ φ) l at_top) :
+  tendsto u at_top at_top :=
+tendsto_at_top_of_monotone_of_filter h (map_ne_bot hl) (tendsto_map' H)
+
 end filter

src/order/filter/bases.lean

@@ -716,7 +716,7 @@ begin
   have lim_uφ : tendsto (u ∘ φ) at_top f,
     from h.tendsto φ_in,
   have lim_φ : tendsto φ at_top at_top,
-    from (tendsto_at_top_mono _ φ_ge tendsto_id),
+    from (tendsto_at_top_mono φ_ge tendsto_id),
   obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, strict_mono ψ ∧ strict_mono (φ ∘ ψ),
     from strict_mono_subseq_of_tendsto_at_top lim_φ,
   exact ⟨φ ∘ ψ, hψφ, lim_uφ.comp $ strict_mono_tendsto_at_top hψ⟩,

src/order/filter/basic.lean

@@ -468,7 +468,7 @@ s.eq_empty_or_nonempty.elim (λ h, absurd hs (h.symm ▸ mt empty_in_sets_eq_bot
 lemma nonempty_of_ne_bot {f : filter α} (hf : f ≠ ⊥) : nonempty α :=
 nonempty_of_exists $ nonempty_of_mem_sets hf univ_mem_sets
 
-lemma filter_eq_bot_of_not_nonempty {f : filter α} (ne : ¬ nonempty α) : f = ⊥ :=
+lemma filter_eq_bot_of_not_nonempty (f : filter α) (ne : ¬ nonempty α) : f = ⊥ :=
 empty_in_sets_eq_bot.mp $ univ_mem_sets' $ assume x, false.elim (ne ⟨x⟩)
 
 lemma forall_sets_nonempty_iff_ne_bot {f : filter α} :
@@ -1795,6 +1795,12 @@ lemma tendsto.eventually {f : α → β} {l₁ : filter α} {l₂ : filter β} {
   ∀ᶠ x in l₁, p (f x) :=
 hf h
 
+@[simp] lemma tendsto_bot {f : α → β} {l : filter β} : tendsto f ⊥ l := by simp [tendsto]
+
+lemma tendsto_of_not_nonempty {f : α → β} {la : filter α} {lb : filter β} (h : ¬nonempty α) :
+  tendsto f la lb :=
+by simp only [filter_eq_bot_of_not_nonempty la h, tendsto_bot]
+
 lemma eventually_eq_of_left_inv_of_right_inv {f : α → β} {g₁ g₂ : β → α} {fa : filter α}
   {fb : filter β} (hleft : ∀ᶠ x in fa, g₁ (f x) = x) (hright : ∀ᶠ y in fb, f (g₂ y) = y)
   (htendsto : tendsto g₂ fb fa) :
@@ -1805,8 +1811,7 @@ lemma tendsto_iff_comap {f : α → β} {l₁ : filter α} {l₂ : filter β} :
   tendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f :=
 map_le_iff_le_comap
 
-lemma tendsto_congr' {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
-  (hl : f₁ =ᶠ[l₁] f₂) :
+lemma tendsto_congr' {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β} (hl : f₁ =ᶠ[l₁] f₂) :
   tendsto f₁ l₁ l₂ ↔ tendsto f₂ l₁ l₂ :=
 by rw [tendsto, tendsto, map_congr hl]
 

src/topology/algebra/ordered.lean

@@ -1870,7 +1870,7 @@ tendsto_nhds_unique at_top_ne_bot (tendsto_at_top_infi_nat f hf)
 /-- $\lim_{x\to+\infty}|x|=+\infty$ -/
 lemma tendsto_abs_at_top_at_top [decidable_linear_ordered_add_comm_group α] :
   tendsto (abs : α → α) at_top at_top :=
-tendsto_at_top_mono _ (λ n, le_abs_self _) tendsto_id
+tendsto_at_top_mono (λ n, le_abs_self _) tendsto_id
 
 local notation `|` x `|` := abs x
 
@@ -1910,3 +1910,37 @@ begin
       have : ∀ b, f b < a' ↔ f b - a < ε, by { intro b, simp [lt_sub_iff_add_lt] },
       simpa only [this] }}
 end
+
+/-!
+Here is a counter-example to a version of the following with `conditionally_complete_lattice α`.
+Take `α = [0, 1) → ℝ` with the natural lattice structure, `ι = ℕ`. Put `f n x = -x^n`. Then
+`⨆ n, f n = 0` while none of `f n` is strictly greater than the constant function `-0.5`.
+-/
+
+lemma tendsto_at_top_csupr {ι α : Type*} [preorder ι] [topological_space α]
+  [conditionally_complete_linear_order α] [order_topology α]
+  {f : ι → α} (h_mono : monotone f) (hbdd : bdd_above $ range f) :
+  tendsto f at_top (𝓝 (⨆i, f i)) :=
+begin
+  by_cases hi : nonempty ι,
+  { resetI,
+    rw tendsto_order,
+    split,
+    { intros a h,
+      cases exists_lt_of_lt_csupr h with N hN,
+      apply eventually.mono (mem_at_top N),
+      exact λ i hi, lt_of_lt_of_le hN (h_mono hi) },
+    { exact λ a h, eventually_of_forall _ (λ n, lt_of_le_of_lt (le_csupr hbdd n) h) } },
+  { exact tendsto_of_not_nonempty hi }
+end
+
+lemma tendsto_at_top_supr {ι α : Type*} [preorder ι] [topological_space α]
+  [complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
+  tendsto f at_top (𝓝 (⨆i, f i)) :=
+tendsto_at_top_csupr h_mono (order_top.bdd_above _)
+
+lemma tendsto_of_monotone {ι α : Type*} [preorder ι] [topological_space α]
+  [conditionally_complete_linear_order α] [order_topology α] {f : ι → α} (h_mono : monotone f) :
+  tendsto f at_top at_top ∨ (∃ l, tendsto f at_top (𝓝 l)) :=
+if H : bdd_above (range f) then or.inr ⟨_, tendsto_at_top_csupr h_mono H⟩
+else or.inl $ tendsto_at_top_at_top_of_monotone' h_mono H