# Zulip Chat Archive

## Stream: new members

### Topic: Harmonic Series Divergence

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

#### Johan Commelin (Jun 22 2020 at 19:46):

I think all of this should go into mathlib

#### Johan Commelin (Jun 22 2020 at 19:46):

Nice work!

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

#### 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 ?

#### 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!

#### Sebastien Gouezel (Jun 22 2020 at 19:51):

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

#### 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 !

#### Patrick Massot (Jun 22 2020 at 19:57):

Why don't you use `begin`

and `end`

?

#### Patrick Massot (Jun 22 2020 at 19:57):

You can `open finset`

and use stuff like `(Ico n (2*n)).sum ...`

.

#### Patrick Massot (Jun 22 2020 at 19:57):

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

#### Sebastien Gouezel (Jun 22 2020 at 19:58):

But using the `big_operators`

sum notation, of course :)

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

#### Patrick Massot (Jun 22 2020 at 19:58):

Yes, even better.

#### Patrick Massot (Jun 22 2020 at 19:59):

Oh, I missed Johan's message.

#### Patrick Massot (Jun 22 2020 at 19:59):

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

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

#### Sebastien Gouezel (Jun 22 2020 at 20:01):

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

#### Reid Barton (Jun 22 2020 at 20:01):

Channel your inner Pascal programmer :upside_down:

#### 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`

?

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

#### Patrick Massot (Jun 22 2020 at 20:21):

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

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

#### 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`

.

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

#### 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
```

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

#### Kenny Lau (Jun 22 2020 at 20:50):

is the non-terminal `field_simp`

ok?

#### Patrick Massot (Jun 22 2020 at 20:51):

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

#### Patrick Massot (Jun 22 2020 at 20:55):

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

.

#### Kenny Lau (Jun 22 2020 at 21:00):

isn't every `field`

a `ring`

? :stuck_out_tongue:

#### Kevin Buzzard (Jun 22 2020 at 21:10):

`field_simp, ring`

made me as happy in 2020 as `ring`

made me in 2018/9.

#### Anatole Dedecker (Jun 22 2020 at 21:15):

Is there a problem with writing `have := ...`

without explicitly writing the goal ?

#### Kenny Lau (Jun 22 2020 at 21:15):

only readability problems

#### Anatole Dedecker (Jun 22 2020 at 21:15):

Ok

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

#### Anatole Dedecker (Jun 22 2020 at 21:20):

Oh indeed

#### Anatole Dedecker (Jun 22 2020 at 21:30):

What is `$`

?

#### Kevin Buzzard (Jun 22 2020 at 21:31):

`X $ Y`

is the same as `X (Y)`

#### Anatole Dedecker (Jun 22 2020 at 21:31):

Oooooooooooh this is great

#### Kevin Buzzard (Jun 22 2020 at 21:31):

it's just a super-low-priority notation

#### Kevin Buzzard (Jun 22 2020 at 21:31):

`#print notation $`

#### Anatole Dedecker (Jun 22 2020 at 21:32):

I was starting to get bored of lisp-like parenthesizing

#### 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 :-)

#### Kevin Buzzard (Jun 22 2020 at 21:32):

I read about it in learnyouahaskell

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

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

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

#### Scott Morrison (Jun 23 2020 at 00:10):

e.g. things like `mono harmonic`

should certainly be their own lemmas.

#### 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
```

#### 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)`

.

#### 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?

#### 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
```

#### Johan Commelin (Jun 23 2020 at 00:57):

You don't want to abuse `1/0 = 0`

? :grinning: :rolling_on_the_floor_laughing:

#### Johan Commelin (Jun 23 2020 at 00:58):

Note that `alternating`

could be done for any `add_comm_group A`

#### Yakov Pechersky (Jun 23 2020 at 00:59):

Well it would mess with what `alternating harmonic`

would converge to.

#### Johan Commelin (Jun 23 2020 at 00:59):

If you replace the `*`

with a `\bu[\Z]`

#### Johan Commelin (Jun 23 2020 at 01:00):

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

#### 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
```

#### Mario Carneiro (Jun 23 2020 at 01:19):

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 (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`

?

#### Mario Carneiro (Jun 23 2020 at 02:40):

Oh I thought you meant standard in maths

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

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

thatdifficult

The first one is definitely there, it's `tendsto_at_top_mono`

. I wouldn't bet on finding the second one.

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

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

#### 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:

#### 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
```

#### Yakov Pechersky (Jun 23 2020 at 14:58):

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

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

#### 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 -> R`

with 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 (Jun 23 2020 at 15:41):

Indeed, everything in the tutorial is too specialized.

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

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

#### Anatole Dedecker (Jun 23 2020 at 20:59):

Patrick Massot said:

Anatole Dedecker said:

Sebastien Gouezel said:

`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

thatdifficultThe 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 (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:

#### Johan Commelin (Jun 29 2020 at 16:26):

Q1: yes

#### 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`

.

#### Anatole Dedecker (Jun 29 2020 at 16:27):

Oh okay

#### Johan Commelin (Jun 29 2020 at 16:27):

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

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

#### Johan Commelin (Jun 29 2020 at 16:29):

I would rename `harmonic`

to `harmonic_series`

, I think. But it's a minor point.

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

#### Patrick Massot (Jun 29 2020 at 16:33):

Put in `topology/order.lean`

only things that involve a topology.

#### Patrick Massot (Jun 29 2020 at 16:33):

The other ones can go in the file defining `at_top`

.

#### Patrick Massot (Jun 29 2020 at 16:34):

`unbounded_of_tensto_at_top`

misses a "d"

#### Patrick Massot (Jun 29 2020 at 16:35):

maybe `tendsto_of_monotone`

is enough for `tendsto_either_of_monotone`

.

#### Patrick Massot (Jun 29 2020 at 16:36):

Why did you put a prime at `harmonic_tendsto_at_top'`

?

#### Anatole Dedecker (Jun 29 2020 at 16:36):

That's a mistake

#### Anatole Dedecker (Jun 29 2020 at 16:36):

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

#### 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 ?

#### Johan Commelin (Jun 29 2020 at 16:42):

Yup, that sounds good

#### Anatole Dedecker (Jun 29 2020 at 16:44):

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

#### Johan Commelin (Jun 29 2020 at 16:45):

Nope

#### Johan Commelin (Jun 29 2020 at 16:45):

So create a big PR

#### Anatole Dedecker (Jun 29 2020 at 16:46):

Okay

#### 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
```

#### Johan Commelin (Jun 29 2020 at 16:47):

If you want to create a smaller first PR

#### Anatole Dedecker (Jun 29 2020 at 17:08):

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

#### Johan Commelin (Jun 29 2020 at 17:15):

First come first serve?

#### Johan Commelin (Jun 29 2020 at 17:15):

But we try to put things that belong together close together

#### Johan Commelin (Jun 29 2020 at 17:15):

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

#### Bryan Gin-ge Chen (Jun 29 2020 at 17:16):

Some files have module docs like: `/-! ### lemmas about foo -/`

that group related lemmas together.

#### Anatole Dedecker (Jun 29 2020 at 17:20):

Oh just realised I meant `topology/algebra/ordered`

not `topology/order`

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

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

#### 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 ?

#### 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 ?

#### Patrick Massot (Jun 29 2020 at 21:33):

Johan is complicating things, one PR will be fine.

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

#### Sebastien Gouezel (Jun 30 2020 at 19:40):

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

.

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

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

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

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

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

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