Harmonic Series Divergence

Stream: new members

[Anatole Dedecker]

Hello again ! Yesterday I discovered the "Formalizing 100 theorem" challenge. Browsing the list, I was surprised to see that no proof was made in Lean of the divergence of the Harmonic Series. I'm glad to say it is now done ! The first two lemmas have been stated and proved by @Patrick Massot in #new_members > sequence_limit_lemmas and I will PR-them to Mathlib as he thinks they should be there. Let me know if you have any ideas about making this shorter, other ways to approach the problem, etc...

import topology.instances.real

open classical filter set topological_space
open_locale topological_space

attribute [instance] classical.prop_decidable

noncomputable theory

-- These two lemmas have been stated and proved by Patrick Massot, and they should soon be PR-ed to mahlib

lemma tendsto_at_top_supr_of_bdd {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [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
  rw tendsto_order,
  split,
  { intros a h,
    rw eventually_at_top,
    cases exists_lt_of_lt_csupr h with N hN,
    exact ⟨N, λ i hi, lt_of_lt_of_le hN (h_mono hi)⟩ },
  { intros a h,
    apply univ_mem_sets',
    intros n,
    exact lt_of_le_of_lt (le_csupr hbdd n) h },
end

lemma tendsto_at_top_of_monotone {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [linear_order α] [topological_space α] [order_topology α] {u : ι → α}
  (h : monotone u) (H : ¬bdd_above (range u)) : tendsto u at_top at_top :=
begin
    rw tendsto_at_top,
    intro b,
    rw mem_at_top_sets,
    rw not_bdd_above_iff at H,
    rcases H b with ⟨_, ⟨N, rfl⟩, hN⟩,
    exact ⟨N, λ n hn, le_of_lt (lt_of_lt_of_le hN $ h hn)⟩,
end

-- Now the theorem in itself

def harmonic (n : ℕ) : ℝ :=
(finset.range n).sum (λ k, 1/(nat.succ k : ℝ))

lemma harmonic_not_tendsto_real (l : ℝ) : ¬ (tendsto harmonic at_top (nhds l)) := by {
    have key : ∀ n : ℕ, 0 < n → 1/2 ≤ harmonic (2*n) - harmonic n, {
        intros n hn,
        rw [(show 2*n = n+n, by linarith), le_sub_iff_add_le, add_comm],
        have := finset.sum_range_add_sum_Ico (λ k, 1/(nat.succ k : ℝ)) (show n ≤ n+n, by linarith),
        change harmonic n + finset.sum (finset.Ico n (n + n)) (λ (k : ℕ), 1 / (nat.succ k : ℝ)) = harmonic (n + n) at this,
        rw ← this,
        have ineq : 1/2 ≤ finset.sum (finset.Ico n (n + n)) (λ (k : ℕ), 1 / (nat.succ k : ℝ)),
        {
            rw (show (1/2 : ℝ) = finset.sum (finset.Ico n (n + n)) (λ (k : ℕ), 1 / (n+n)), by {
                rw [finset.sum_const, finset.Ico.card, (show n+n-n = n, by simp),
                    nsmul_eq_mul, ← div_eq_mul_one_div, ← two_mul,
                    mul_comm, div_mul_eq_div_mul_one_div, div_self],
                simp,
                norm_cast, change (n ≠ 0), symmetry, exact ne_of_lt hn,
            }),
            apply finset.sum_le_sum,
            intros x hx,
            simp at hx,
            rw one_div_le_one_div,
            norm_cast, exact nat.succ_le_of_lt hx.2,
            norm_cast, linarith,
            norm_cast, exact nat.zero_lt_succ x,
        },
        rwa add_le_add_iff_left,
    },
    by_contra h,
    have : (1/2 : ℝ) ≤ 0, {
        apply @ge_of_tendsto _ _ _ _ _ (λ n, (harmonic ∘ (λ k, 2*k)) n - harmonic n) _ _ at_top,
        exact at_top_ne_bot,
        rw (show 0 = l-l, by linarith),
        apply tendsto.sub,
        {
            simp,
            apply tendsto.comp,
            exact h,
            rw tendsto_at_top,
            simp,
            intros b,
            use b,
            intros c h,
            linarith,
        },
        exact h,
        apply eventually_at_top.mpr,
        use (nat.succ 0),
        intros n hn,
        exact (key n (by linarith)),
        use 0,
    },
    linarith,
}

theorem harmonic_tendsto_at_top : tendsto harmonic at_top at_top := by {
    have : monotone harmonic, {
        intros p q hpq,
        unfold harmonic,
        apply finset.sum_le_sum_of_subset_of_nonneg,
        rwa finset.range_subset,
        intros x h _,
        apply le_of_lt,
        apply one_div_pos_of_pos,
        norm_cast,
        exact nat.zero_lt_succ _,
    },
    by_cases H : bdd_above (range harmonic), {
        exfalso,
        exact harmonic_not_tendsto_real (supr harmonic) (tendsto_at_top_supr_of_bdd this H),
    }, {
        exact tendsto_at_top_of_monotone this H,
    }
}

[Johan Commelin]

I think all of this should go into mathlib

[Johan Commelin]

Nice work!

[Johan Commelin]

Quick feedback (for mathlib submission):

• indent by 2 spaces
• closing brace } on same line as last tactic in the block
• don't use simp halfway a proof. Use squeeze_simp to get a simp only version
• if you open_locale big_operators then you can write \sum i in finset.range n, blabla i for nice notation.

[Anatole Dedecker]

Thanks ! I can't find a situation where it would help proving something else though, so should it really go into mathlib ?

[Sebastien Gouezel]

I feel you can get a slightly slicker proof, avoiding all arguments by contradiction, by noting that harmonic (2^n) \geq n/2 (you have proved this) and therefore harmonic (2^n) tends to infinity (as it is bounded below by a sequence tending to infinity -- I hope we have this!). And then, for a monotone sequence, having a subsequence tending to infinity implies convergence to infinity (I hope we have this also). But what you did is great!

[Sebastien Gouezel]

This is so important that it should definitely go into mathlib!

[Anatole Dedecker]

Oh yeah using 2^n is smart, I'm going to try it. Thanks for the feedback !

[Patrick Massot]

Why don't you use begin and end?

[Patrick Massot]

You can open finset and use stuff like (Ico n (2*n)).sum ....

[Patrick Massot]

or def harmonic (n : ℕ) : ℝ := (range n).sum (λ k, 1/(k + 1 : ℝ))

[Sebastien Gouezel]

But using the big_operators sum notation, of course :)

[Sebastien Gouezel]

As explained in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Harmonic.20Series.20Divergence/near/201652128

[Patrick Massot]

Yes, even better.

[Patrick Massot]

Oh, I missed Johan's message.

[Patrick Massot]

You'll get maximal readability by using advice from both.

[Anatole Dedecker]

Patrick Massot said:

Why don't you use begin and end?

C++ part of me wants {} around blocks, so I like the by syntax. But I can change it of course

[Sebastien Gouezel]

You should work on the LaTeX part of you :-)

[Reid Barton]

Channel your inner Pascal programmer :upside_down:

[Anatole Dedecker]

If this gets in mathlib, do you think I should make ∀ n : ℕ, 0 < n → 1/2 ≤ harmonic (2*n) - harmonic n a lemma by itself ? Or keep it as a have ?

[Patrick Stevens]

Aside: we don't have the Cauchy condensation test for series convergence, do we - in fact I couldn't really find anything about the convergence of series, although my mathlib-fu is still not good

[Patrick Massot]

Yes, I've already said we should develop some basics of convergence of series.

[Kenny Lau]

My understanding is this -- someone goes "let's prove theorems about convergence of series" and then someone else goes "oh this is all just a special case of some lemma about filter" so we prove everything about filters but nobody has specialized them to series yet

[Sebastien Gouezel]

We have a bunch on infinite sums, but almost nothing specialized to the case where the infinite sum is indexed by ℕ. See topology/algebra/infinite_sum.lean.

[Sebastien Gouezel]

Anatole Dedecker said:

If this gets in mathlib, do you think I should make ∀ n : ℕ, 0 < n → 1/2 ≤ harmonic (2*n) - harmonic n a lemma by itself ? Or keep it as a have ?

I would say have it as a separate lemma.

[Patrick Massot]

@Anatole Dedecker Of course I agree with Sébastien that you should directly prove that harmonic goes to infinity. But I made a compression pass on your proof (without changing the proof on paper) because I think you could learn various tricks by studying the differences with your proof. You need to replace the top import with analysis.specific_limits. Then you can do:

open finset
open_locale big_operators

def harmonic (n : ℕ) := ∑ k in range n, 1/(k + 1 : ℝ)

lemma harmonic_not_tendsto_real (l : ℝ) : ¬ (tendsto harmonic at_top (nhds l)) :=
begin
  have key : ∀ n > 0, 1/2 ≤ harmonic (2*n) - harmonic n,
  { intros n hn,
    suffices : harmonic n + 1 / 2 ≤ harmonic (n + n),
    { rw two_mul,
      linarith },
    have : harmonic n + ∑ k in Ico n (n + n), 1/(k + 1 : ℝ) = harmonic (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,
    { rw [sum_const, Ico.card],
      field_simp [show (n : ℝ) + n ≠ 0, by norm_cast ; linarith],
      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 } },
  by_contra h,
  have ineq : ∀ᶠ (c : ℕ) in at_top, 1 / (2 : ℝ) ≤ harmonic (2 * c) - harmonic c :=
    eventually_at_top.mpr ⟨1, λ n hn, key n (by linarith)⟩,
  suffices : tendsto (λ (n : ℕ), (harmonic ∘ λ (k : ℕ), 2 * k) n - harmonic n) at_top (𝓝 0),
    by linarith [ge_of_tendsto at_top_ne_bot this ineq],
  convert (h.comp $ tendsto_at_top_mul_left two_pos tendsto_id).sub h,
  simp
end

[Patrick Massot]

You can use https://leanprover-community.github.io/mathlib_docs/tactics.html to learn about any tactic that you don't know yet.

[Kenny Lau]

is the non-terminal field_simp ok?

[Patrick Massot]

I think so, this tactic is really meant as a preprocessing step.

[Patrick Massot]

I've slightly edited the proof to adhere strictly to the idiomatic field_simp, ring.

[Kenny Lau]

isn't every field a ring? :stuck_out_tongue:

[Kevin Buzzard]

field_simp, ring made me as happy in 2020 as ring made me in 2018/9.

[Anatole Dedecker]

Is there a problem with writing have := ... without explicitly writing the goal ?

[Kenny Lau]

only readability problems

[Anatole Dedecker]

Ok

[Patrick Massot]

I replaced that because you wrote change ... at this right after this line. So I only combined two of your lines into one.

[Anatole Dedecker]

Oh indeed

[Anatole Dedecker]

What is $ ?

[Kevin Buzzard]

X $ Y is the same as X (Y)

[Anatole Dedecker]

Oooooooooooh this is great

[Kevin Buzzard]

it's just a super-low-priority notation

[Kevin Buzzard]

#print notation $

[Anatole Dedecker]

I was starting to get bored of lisp-like parenthesizing

[Kevin Buzzard]

the 1 and 0 just indicate that it gets evaluated last, and when it gets evaluated Lean discovers that it doesn't do anything :-)

[Kevin Buzzard]

I read about it in learnyouahaskell

[Anatole Dedecker]

Kevin Buzzard said:

the 1 and 0 just indicate that it gets evaluated last, and when it gets evaluated Lean discovers that it doesn't do anything :-)

Smart

[Anatole Dedecker]

Sebastien Gouezel said:

I feel you can get a slightly slicker proof, avoiding all arguments by contradiction, by noting that harmonic (2^n) \geq n/2 (you have proved this) and therefore harmonic (2^n) tends to infinity (as it is bounded below by a sequence tending to infinity -- I hope we have this!). And then, for a monotone sequence, having a subsequence tending to infinity implies convergence to infinity (I hope we have this also). But what you did is great!

Well, I I'd be done if I had found those two lemmas... If they exist, they are well hidden. I'll continue to search tomorrow, and if they don't exist I'll prove them, it doesn't seem that difficult

[Scott Morrison]

For readability you might like to factor out more steps into lemmas. Essentially any top level have statement in a long proof is a good candidate for extraction.

[Scott Morrison]

e.g. things like mono harmonic should certainly be their own lemmas.

[Johan Commelin]

Does it make sense to

-- the sequence
def harmonic (n : nat) : real := 1 / n

def series {A : Type*} [add_comm_monoid A] (sequence : nat → A) :=
\sum i in finset.range n, sequence i

-- the series
def harmonic_series := series harmonic

[Johan Commelin]

Then we can prove things about 1 + (1/2)^2 + (1/3)^2 + ... later as things about series (square \circ harmonic).

[Yakov Pechersky]

How about (n : \Z) so that one can have alternating harmonic? Or should alternating_series be a separate sum?

[Yakov Pechersky]

def harmonic (n : nat) : real := 1 / (n + 1)

def alternating (n : nat) (series : nat -> real) : real := (-1 ^ (n+1)) * series n

[Johan Commelin]

You don't want to abuse 1/0 = 0? :grinning: :rolling_on_the_floor_laughing:

[Johan Commelin]

Note that alternating could be done for any add_comm_group A

[Yakov Pechersky]

Well it would mess with what alternating harmonic would converge to.

[Johan Commelin]

If you replace the * with a \bu[\Z]

[Johan Commelin]

/me doesn't know that standard indexing convention for standard series

[Yakov Pechersky]

def alternating {r : Type*} [add_comm_group r] (n : nat) (series : nat -> r) : r := (-1 ^ (n+1)) \bu[\Z] series n

[Mario Carneiro]

The indexing convention is whatever makes the result cleanest. $\sum_{n=1}^\infty\frac1{n^2}=\pi^2/6$ but $\sum_{n=0}^\infty a^n=1/(1-a)$

[Johan Commelin]

You can start the first sum at 0 as well, right? Or am I misunderstanding when to abuse 1/0 = 0?

[Mario Carneiro]

Oh I thought you meant standard in maths

[Mario Carneiro]

I don't see a problem with starting the sum at 0 in lean as long as it's still true

[Patrick Massot]

Anatole Dedecker said:

Sebastien Gouezel said:

I feel you can get a slightly slicker proof, avoiding all arguments by contradiction, by noting that harmonic (2^n) \geq n/2 (you have proved this) and therefore harmonic (2^n) tends to infinity (as it is bounded below by a sequence tending to infinity -- I hope we have this!). And then, for a monotone sequence, having a subsequence tending to infinity implies convergence to infinity (I hope we have this also). But what you did is great!

Well, I I'd be done if I had found those two lemmas... If they exist, they are well hidden. I'll continue to search tomorrow, and if they don't exist I'll prove them, it doesn't seem that difficult

The first one is definitely there, it's tendsto_at_top_mono. I wouldn't bet on finding the second one.

[Patrick Massot]

lemma unbounded_of_tensto_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⟩,
  rw tendsto_at_top at h,
  cases no_top M with M' hMM',
  cases mem_at_top_sets.mp (h M') with a ha,
  apply lt_irrefl M,
  calc
  M < M' : hMM'
  ... ≤ f a : ha a (le_refl _)
  ... ≤ M : hM (set.mem_range_self a)
end

lemma tendsto_at_top_of_monotone_of_subseq {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [linear_order α] [no_top_order α] {u : ι → α}
  {φ : ι → ι} (h : monotone u) (H : tendsto (u ∘ φ) at_top at_top) : tendsto u at_top at_top :=
begin
  apply tendsto_at_top_of_monotone h,
  suffices : ¬ bdd_above (range $ u ∘ φ),
  { contrapose! this,
    exact bdd_above.mono (range_comp_subset_range φ u) this },
  exact unbounded_of_tensto_at_top H,
end

while writing this I also noticed I had a couple of copy-paste typos in yesterday's lemmas (unnecessary [topological_space α] [order_topology α] in lemmas that don't use any topology, only the order).

[Anatole Dedecker]

Big thanks to everyone for your help and advice ! I was also thinking of defining series in general as @Johan Commelin proposed, but I thought a more generic and complete had to exist in mathlib. If this isn't the case, it would indeed be interesting to define it !

I have to admit I didn't think this project would get to mathlib, so making it clean and user-friendly wasn't my primary goal, but now I feel this is even more rewarding than the challenge in itself ! I'll finish the shorter proof with 2^n and then I'll work on organizing everything, breaking into lemmas, etc...

[Anatole Dedecker]

Well, I'll actually have to pause lean for a few days after that, cause I'm supposed to prepare an unofficial CS "lecture" for my colleagues :laughing:

[Anatole Dedecker]

With Patrick's lemmas in not_yet_in_lib, this is where I am now :

import analysis.specific_limits

import not_yet_in_lib

open classical filter finset set topological_space
open_locale topological_space big_operators

attribute [instance] classical.prop_decidable

noncomputable theory

def harmonic (n : ℕ) : ℝ :=
∑ i in range n, 1/(i.succ : ℝ)

lemma mono_harmonic : monotone harmonic :=
begin
  intros p q hpq,
  unfold harmonic,
  apply sum_le_sum_of_subset_of_nonneg,
  rwa range_subset,
  intros x h _,
  apply le_of_lt,
  apply one_div_pos_of_pos,
  norm_cast,
  exact nat.zero_lt_succ _,
end

lemma half_le_harmonic_double_sub_harmonic (n : ℕ) (hn : 0 < n) : 1/2 ≤ harmonic (2*n) - harmonic n :=
begin
  suffices : harmonic n + 1 / 2 ≤ harmonic (n + n),
    { rw two_mul,
      linarith },
    have : harmonic n + ∑ k in Ico n (n + n), 1/(k + 1 : ℝ) = harmonic (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 harmonic_two_pow_ge_id_div_two (n : ℕ) : (n / 2 : ℝ) ≤ harmonic (2^n) :=
begin
  induction n with n hn,
  unfold harmonic,
  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],
  linarith,
  have : harmonic (2^n) + 1 / 2 ≤ harmonic (2^n.succ),
  { 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

lemma harmonic_two_pow_ge_id_div_two' : (λ n : ℕ, (n/2 : ℝ)) ≤ (λ n : ℕ, harmonic (2^n)) :=
begin
  intros n,
  simp only [harmonic_two_pow_ge_id_div_two],
end

theorem harmonic_tendsto_at_top : tendsto harmonic at_top at_top :=
begin
  suffices : tendsto (λ n : ℕ, harmonic (2^n)) at_top at_top, by
  { apply tendsto_at_top_of_monotone_of_subseq mono_harmonic this},
  apply tendsto_at_top_mono,
  exact harmonic_two_pow_ge_id_div_two',
  apply tendsto_at_top_div,
  linarith,
  exact tendsto_coe_nat_real_at_top_at_top,
end

[Yakov Pechersky]

If I recall correctly, the tutorial project has a lemma about subsequences that tend to infinity

[Yakov Pechersky]

Seems like I remembered somewhat right, but they are in the opposite direction: https://github.com/leanprover-community/tutorials/blob/13efdfcc7879582710bb541c1b691d8e2b65fec9/src/solutions/09_limits_final.lean#L217

[Anatole Dedecker]

Yakov Pechersky said:

If I recall correctly, the tutorial project has a lemma about subsequences that tend to infinity

Indeed, all these lemmas are easy to prove for the specific case of N -> Rwith epsilon-delta limits (I did indeed prove everything in this tutorial since it is more or less the same content as the course I took with Patrick Massot). But I wanted to use mathlib as much as possible to avoid unnecessary dependencies

[Patrick Massot]

Indeed, everything in the tutorial is too specialized.

[Patrick Massot]

I also need to find time to remove the mess in tuto_lib now that Bolzano-Weirstrass is in mathlib.

[Patrick Massot]

There is even more mess there that I remembered. I shouldn't draw attention to this file.

[Anatole Dedecker]

Patrick Massot said:

Anatole Dedecker said:

Sebastien Gouezel said:

I feel you can get a slightly slicker proof, avoiding all arguments by contradiction, by noting that harmonic (2^n) \geq n/2 (you have proved this) and therefore harmonic (2^n) tends to infinity (as it is bounded below by a sequence tending to infinity -- I hope we have this!). And then, for a monotone sequence, having a subsequence tending to infinity implies convergence to infinity (I hope we have this also). But what you did is great!

Well, I I'd be done if I had found those two lemmas... If they exist, they are well hidden. I'll continue to search tomorrow, and if they don't exist I'll prove them, it doesn't seem that difficult

The first one is definitely there, it's tendsto_at_top_mono. I wouldn't bet on finding the second one.

The fun thing is : I had seen this lemma. I just hadn't thought what I was searching was a certain function being monotonous

[Anatole Dedecker]

Ok so I'm reviving this topic cause this will be my first ever commit to mathlib, and I'm a bit nervous :sweat_smile: To sum up, I currently have the following lemmas (and their proofs, which I didn't wrote here for readability as I assume they'll be reviewed later anyway, but you can find them at https://gitlab.com/Someody42/harmonic ) :

--Patrick's lemmas

lemma tendsto_at_top_supr_of_bdd {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [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)) := sorry

lemma tendsto_at_top_of_monotone {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [linear_order α] {u : ι → α}
  (h : monotone u) (H : ¬bdd_above (range u)) : tendsto u at_top at_top := sorry

lemma unbounded_of_tensto_at_top {α β : Type*} [nonempty α] [semilattice_sup α]
  [preorder β] [no_top_order β]
  {f : α → β} (h : tendsto f at_top at_top) : ¬ bdd_above (range f) := sorry

lemma tendsto_at_top_of_monotone_of_subseq {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [linear_order α] [no_top_order α] {u : ι → α}
  {φ : ι → ι} (h : monotone u) (H : tendsto (u ∘ φ) at_top at_top) : tendsto u at_top at_top := sorry

-- My lemmas

lemma tendsto_either_of_monotone {ι  : Type*} [nonempty ι] [semilattice_sup ι]
  {α : Type*} [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)) := sorry

def harmonic (n : ℕ) : ℝ :=
∑ i in range n, 1/(i.succ : ℝ)

lemma mono_harmonic : monotone harmonic := sorry

lemma half_le_harmonic_double_sub_harmonic (n : ℕ) (hn : 0 < n) : 1/2 ≤ harmonic (2*n) - harmonic n := sorry

lemma harmonic_two_pow_ge_id_div_two (n : ℕ) : (n / 2 : ℝ) ≤ harmonic (2^n) := sorry

lemma harmonic_two_pow_ge_id_div_two' : (λ n : ℕ, (n/2 : ℝ)) ≤ (λ n : ℕ, harmonic (2^n)) := sorry

theorem harmonic_tendsto_at_top : tendsto harmonic at_top at_top := sorry

My questions are :

• Do all of these lemmas have their place in mathlib ?
• I was thinking of putting the "generic" ones in topology/order.lean as Patrick advised for the first two, do they all fit there ?
• Maybe there could be a better name than tendsto_either_of_monotone ?
• Where should I put the harmonic stuff ? I was thinking of analysis/specific_limits but maybe not all of the intermediary lemmas fit here ?
• Should I make two separates PR, one for generic lemmas and the other for harmonic series ?
• Do I need to write some doc ?

Thanks in advance ! Sorry for asking so many things, I want to do things right :sweat_smile:

[Johan Commelin]

Q1: yes

[Johan Commelin]

Please don't write i.succ. For simp it's a lot better if you use i+1.

[Anatole Dedecker]

Oh okay

[Johan Commelin]

If it's < 100 lines, put everything in 1 PR. Otherwise splitting makes sense.

[Johan Commelin]

Do I need to write some doc ?

Definitions need docstrings. Otherwise, this won't need to many docs.

[Johan Commelin]

I would rename harmonic to harmonic_series, I think. But it's a minor point.

[Johan Commelin]

@Anatole Dedecker Let me know if you want guidance on the git side of creating a PR.

[Patrick Massot]

Put in topology/order.lean only things that involve a topology.

[Patrick Massot]

The other ones can go in the file defining at_top.

[Patrick Massot]

unbounded_of_tensto_at_top misses a "d"

[Patrick Massot]

maybe tendsto_of_monotone is enough for tendsto_either_of_monotone.

[Patrick Massot]

Why did you put a prime at harmonic_tendsto_at_top'?

[Anatole Dedecker]

That's a mistake

[Anatole Dedecker]

It's because I kept other versions of the proof in the same file

[Anatole Dedecker]

Johan Commelin said:

Anatole Dedecker Let me know if you want guidance on the git side of creating a PR.

Patrick gave me write access to non-master branch, so if I understand well I just have to follow the steps here : https://leanprover-community.github.io/contribute/index.html ?

[Johan Commelin]

Yup, that sounds good

[Anatole Dedecker]

Can I make the two PRs without creating two local branches ?

[Johan Commelin]

Nope

[Johan Commelin]

So create a big PR

[Anatole Dedecker]

Okay

[Johan Commelin]

And then you can do

git checkout -b harmonic-preparations
git checkout harmonic-main-branch -- src/topology/foobar.lean
...
git commit -am "feat(*): preparations for divergence of harmonic series"
git push
# create another PR

[Johan Commelin]

If you want to create a smaller first PR

[Anatole Dedecker]

Is there any logic in the way we order things in a file ?

[Johan Commelin]

First come first serve?

[Johan Commelin]

But we try to put things that belong together close together

[Johan Commelin]

And sometimes we turn a file upside down and inside out, when it becomes too messy.

[Bryan Gin-ge Chen]

Some files have module docs like: /-! ### lemmas about foo -/ that group related lemmas together.

[Anatole Dedecker]

Oh just realised I meant topology/algebra/ordered not topology/order

[Patrick Massot]

Bryan Gin-ge Chen said:

Some files have module docs like: /-! ### lemmas about foo -/ that group related lemmas together.

Note that you new line breaks before and after the title.

[Bryan Gin-ge Chen]

Yes, that's recommended. Although if everything fits on one line then it's strictly not necessary.

[Anatole Dedecker]

Johan Commelin said:

And then you can do

git checkout -b harmonic-preparations
git checkout harmonic-main-branch -- src/topology/foobar.lean
...
git commit -am "feat(*): preparations for divergence of harmonic series"
git push
# create another PR

Hmmmmm I think I misunderstood something here :sweat_smile: In which order was I supposed to do the operations ?

[Anatole Dedecker]

I mean : should I do all modifications first and then checkout ? Or just the modifications I want to put in the first PR ?

[Patrick Massot]

Johan is complicating things, one PR will be fine.

[Anatole Dedecker]

Just to be sure : is there any part of Mathlib dedicated to series ? @Sebastien Gouezel mentioned topology.algebra.infinite_sums but that doesn't seem to be what I'm searching for.

[Sebastien Gouezel]

The natural place in mathlib would probably be analysis/specific_limits.

[Anatole Dedecker]

Oh yeah, but at the moment is there anything done ? Because @Yury G. Kudryashov suggested me to extend the result to p-series by proving Cauchy Condensation Test, and I didn't know if there were any infrastructure I should base on top of

[Sebastien Gouezel]

I don't think there is anything else specifically on series. It might be time to start a new file in this direction.

[Patrick Massot]

Yes, this was discussed before. We have many things about sumable families of elements of a topological additive monoid, but nothing about series. Of course we can already write partial sums and speak about their limits, but I think we need a dedicated set of lemmas, including convergence criteria (there are many more common criteria than Cauchy condensation).

[Patrick Massot]

One slightly painful question is whether we should impose the source type. It is tempting to use series whose general term is indexed by natural numbers, but sometimes it's much more natural to have something slightly smaller or bigger. I would say any source type that has a reasonable at_top filter should be supported. Also convergence should probably be expressed for an arbitrary filter on the target, but then we run into the issue that we want to call diverging a series which converges to at_top on the target...

[Anatole Dedecker]

Hmmmm not sure about being well placed to make these design choices then. But if someone wants to setup basic definitions, I think I'll be able to prove a decent amount of things

[Patrick Massot]

Sure, I wasn't writing this specifically for you. I hope that Sébastien and Yury will comment on this (we should probably move this to the math stream) and then we can write the definitions and let everybody contribute lemmas.