Zulip Chat Archive

Stream: new members

Topic: Harmonic Series Divergence


view this post on Zulip Anatole Dedecker (Jun 22 2020 at 19:45):

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,
    }
}

view this post on Zulip Johan Commelin (Jun 22 2020 at 19:46):

I think all of this should go into mathlib

view this post on Zulip Johan Commelin (Jun 22 2020 at 19:46):

Nice work!

view this post on Zulip Johan Commelin (Jun 22 2020 at 19:48):

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.

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 19:49):

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

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 19:50):

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!

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 19:51):

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

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 19:55):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 19:57):

Why don't you use begin and end?

view this post on Zulip Patrick Massot (Jun 22 2020 at 19:57):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 19:57):

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

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 19:58):

But using the big_operators sum notation, of course :)

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 19:58):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 19:58):

Yes, even better.

view this post on Zulip Patrick Massot (Jun 22 2020 at 19:59):

Oh, I missed Johan's message.

view this post on Zulip Patrick Massot (Jun 22 2020 at 19:59):

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

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 20:00):

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

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 20:01):

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

view this post on Zulip Reid Barton (Jun 22 2020 at 20:01):

Channel your inner Pascal programmer :upside_down:

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 20:18):

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 ?

view this post on Zulip Patrick Stevens (Jun 22 2020 at 20:20):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 20:21):

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

view this post on Zulip Kenny Lau (Jun 22 2020 at 20:30):

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

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 20:32):

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.

view this post on Zulip Sebastien Gouezel (Jun 22 2020 at 20:32):

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.

view this post on Zulip Patrick Massot (Jun 22 2020 at 20:46):

@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

view this post on Zulip Patrick Massot (Jun 22 2020 at 20:48):

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

view this post on Zulip Kenny Lau (Jun 22 2020 at 20:50):

is the non-terminal field_simp ok?

view this post on Zulip Patrick Massot (Jun 22 2020 at 20:51):

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

view this post on Zulip Patrick Massot (Jun 22 2020 at 20:55):

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

view this post on Zulip Kenny Lau (Jun 22 2020 at 21:00):

isn't every field a ring? :stuck_out_tongue:

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:10):

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

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:15):

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

view this post on Zulip Kenny Lau (Jun 22 2020 at 21:15):

only readability problems

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:15):

Ok

view this post on Zulip Patrick Massot (Jun 22 2020 at 21:18):

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

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:20):

Oh indeed

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:30):

What is $ ?

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:31):

X $ Y is the same as X (Y)

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:31):

Oooooooooooh this is great

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:31):

it's just a super-low-priority notation

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:31):

#print notation $

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:32):

I was starting to get bored of lisp-like parenthesizing

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:32):

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

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 21:32):

I read about it in learnyouahaskell

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 21:32):

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

view this post on Zulip Anatole Dedecker (Jun 22 2020 at 22:35):

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

view this post on Zulip Scott Morrison (Jun 23 2020 at 00:09):

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.

view this post on Zulip Scott Morrison (Jun 23 2020 at 00:10):

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 00:46):

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 00:46):

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

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 00:52):

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

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 00:54):

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

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 00:57):

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 00:58):

Note that alternating could be done for any add_comm_group A

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 00:59):

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 00:59):

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 01:00):

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

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 01:00):

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

view this post on Zulip Mario Carneiro (Jun 23 2020 at 01:19):

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

view this post on Zulip Johan Commelin (Jun 23 2020 at 02:19):

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

view this post on Zulip Mario Carneiro (Jun 23 2020 at 02:40):

Oh I thought you meant standard in maths

view this post on Zulip Mario Carneiro (Jun 23 2020 at 02:40):

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

view this post on Zulip Patrick Massot (Jun 23 2020 at 06:57):

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.

view this post on Zulip Patrick Massot (Jun 23 2020 at 07:06):

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).

view this post on Zulip Anatole Dedecker (Jun 23 2020 at 12:13):

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...

view this post on Zulip Anatole Dedecker (Jun 23 2020 at 12:30):

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:

view this post on Zulip Anatole Dedecker (Jun 23 2020 at 12:46):

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

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 14:58):

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

view this post on Zulip Yakov Pechersky (Jun 23 2020 at 15:31):

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

view this post on Zulip Anatole Dedecker (Jun 23 2020 at 15:41):

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

view this post on Zulip Patrick Massot (Jun 23 2020 at 15:41):

Indeed, everything in the tutorial is too specialized.

view this post on Zulip Patrick Massot (Jun 23 2020 at 15:54):

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

view this post on Zulip Patrick Massot (Jun 23 2020 at 15:55):

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

view this post on Zulip Anatole Dedecker (Jun 23 2020 at 20:59):

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

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:21):

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:

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:26):

Q1: yes

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:27):

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

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:27):

Oh okay

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:27):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:28):

Do I need to write some doc ?

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:29):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:31):

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

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:33):

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

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:33):

The other ones can go in the file defining at_top.

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:34):

unbounded_of_tensto_at_top misses a "d"

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:35):

maybe tendsto_of_monotone is enough for tendsto_either_of_monotone.

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:36):

Why did you put a prime at harmonic_tendsto_at_top'?

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:36):

That's a mistake

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:36):

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

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:40):

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 ?

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:42):

Yup, that sounds good

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:44):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:45):

Nope

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:45):

So create a big PR

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 16:46):

Okay

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:46):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:47):

If you want to create a smaller first PR

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 17:08):

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

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:15):

First come first serve?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:15):

But we try to put things that belong together close together

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:15):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:16):

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

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 17:20):

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

view this post on Zulip Patrick Massot (Jun 29 2020 at 17:59):

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.

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 18:09):

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

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 21:26):

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 ?

view this post on Zulip Anatole Dedecker (Jun 29 2020 at 21:30):

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

view this post on Zulip Patrick Massot (Jun 29 2020 at 21:33):

Johan is complicating things, one PR will be fine.

view this post on Zulip Anatole Dedecker (Jun 30 2020 at 19:33):

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.

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 19:40):

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

view this post on Zulip Anatole Dedecker (Jun 30 2020 at 19:43):

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

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 19:44):

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

view this post on Zulip Patrick Massot (Jun 30 2020 at 21:56):

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).

view this post on Zulip Patrick Massot (Jun 30 2020 at 22:00):

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...

view this post on Zulip Anatole Dedecker (Jun 30 2020 at 23:12):

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

view this post on Zulip Patrick Massot (Jun 30 2020 at 23:20):

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.


Last updated: May 13 2021 at 18:26 UTC