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

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

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

#### 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),
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],

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

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

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.

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

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 ?

Nope

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

So create a big PR

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