feat(analysis/alt_series): add alternating series test

[ecstatic-morse]

Prove that alternating series satisfy the Cauchy criterion. Unfortunately, they are not summable because summable requires absolute convergence.

---

👋 New contributor here! Please let me know if I've made any style mistakes, documentation errors or proved something inefficiently. I'm trying to get better.

From this Zulip conversation, it seems like equivalents for has_sum, tsum and summable are needed that work for conditionally convergent sequences. I'm not quite sure what those definitions should look like—this is my first mathlib contribution—so I've omitted them for now. Once they are added it will be trivial to use alternating_partial_sum_is_cauchy_seq to prove that they hold for alternating series.

I've put this file next to the one for p_series for now, let me know if there's somewhere better.

[kmill]

I can't comment on how this all fits into analysis (that's not my expertise), but here are some suggestions for structuring proofs.

[kmill]

even.neg_one_pow_add_right and even.neg_one_pow_add_left? This seems to roughly match naming of other things in this file, though it diverges from neg_one_pow_of_even and such.

[kmill]

When I was testing this I had put the lemmas into the global namespace accidentally where the dot notation does work, but I see it doesn't because it's in the nat namespace. That's too bad.

[kmill]

I forgot last night that you can give an expression to simpa:

Suggested change

	have hcs := alternating_partial_sum_is_cau_seq a ha_tendsto_zero ha_anti ha_nonneg,
	simpa only [abs_sub_comm] using hcs,
	simpa only [abs_sub_comm]
	using alternating_partial_sum_is_cau_seq a ha_tendsto_zero ha_anti ha_nonneg,

Another thing you can do is

Suggested change

	have hcs := alternating_partial_sum_is_cau_seq a ha_tendsto_zero ha_anti ha_nonneg,
	simpa only [abs_sub_comm] using hcs,
	have := alternating_partial_sum_is_cau_seq a ha_tendsto_zero ha_anti ha_nonneg,
	simpa only [abs_sub_comm],

since simpa defaults to looking at this.

[PatrickMassot]

Thanks! I've suggested a simpler proof. Many intermediate lemmas are not needed at all. Also you should move stupid supporting lemmas (like your nat.antitone_suffix) to their natural location with natural assumptions and names, otherwise people will keep reproving them.

[PatrickMassot]

This is a weird description since nothing prevents a 0 to be negative in this definition. I really don't see why you need two definitions. The second one is obviously the opposite of the first one.

[PatrickMassot]

I don't think this is worth a new file that will be hard to find. It could go with the other specific limits (but this isn't a hard requirement).

[PatrickMassot]

This has nothing to do in this file. And it's very easy to generalize without being harder to use. You can write:

@[to_additive]
lemma antitone.mul_const_left {α β : Type*} [has_mul α] [preorder α]
  [covariant_class α α (*) (≤)] [preorder β] {u : α → β} (hu : antitone u) (a₀ : α) : 
antitone (λ a, u $ a₀ * a) :=
λ x y hx, hu (mul_le_mul_left' hx a₀)

@[to_additive]
lemma antitone.mul_const_right {α β : Type*} [has_mul α] [preorder α]
  [covariant_class α α (function.swap (*)) (≤)] [preorder β] {u : α → β} (hu : antitone u) (a₀ : α) : 
antitone (λ a, u $ a * a₀) :=
λ x y hx, hu (mul_le_mul_right' hx a₀)

This can probably go in the same file as mul_le_mul_left' unless antitone is not available there. You can also have the same lemma with monotone of course.

[urkud]

Or have lemmas that state monotonicity of (*) a and (* a), then use antitone.comp_monotone _.

[ecstatic-morse]

See #11815.

[PatrickMassot]

I think this lemma is not necessary.

[PatrickMassot]

I think this lemma is not necessary.

[PatrickMassot]

This proof is needlessly complicated (if you count all lemmas that are used only to prove it). I think you should add in topology.metric.basic, right after metric.cauchy_seq_iff':

lemma cauchy_seq_of_le_tendsto_0' {α β : Type*} [pseudo_metric_space α] [nonempty β]
  [semilattice_sup β] {s : β → α} {b : β → ℝ}
    (h : ∀ {n m}, n ≤ m → dist (s n) (s m) ≤ b n) (h' : tendsto b at_top (𝓝 0)) :
    cauchy_seq s :=
begin
  rw metric.cauchy_seq_iff,
  intros ε ε_pos,
  obtain ⟨N, hN⟩ : ∃ n, ∀ m ≥ n, b n < ε/2,
  { obtain ⟨N, hN⟩ :=
     eventually_at_top.mp ((nhds_basis_zero_abs_sub_lt ℝ).tendsto_right_iff.mp h' _ $ half_pos ε_pos),
    exact ⟨N, λ m hm, lt_of_abs_lt (hN N le_rfl)⟩ },
  use N,
  intros n hn m hm,
  calc dist (s n) (s m) ≤ dist (s n) (s N) + dist (s N) (s m) : dist_triangle _ _ _
  ... = dist (s N) (s n) + dist (s N) (s m) : by rw dist_comm
  ... < ε : by linarith [h hn, h hm, hN n hn, hN m hm]
end

and then prove the above theorem using only alternating_partial_sum_nonneg and alternating_partial_sum_le_first (and the renamed antitone.add_const_left from above):

theorem alternating_partial_sum_is_cauchy_seq (ha_tendsto_zero : tendsto a at_top (𝓝 0))
  (ha_anti : antitone a) (ha_nonneg : ∀ n, 0 ≤ a n) : cauchy_seq (alternating_partial_sum a) :=
begin
  apply cauchy_seq_of_le_tendsto_0' _ ha_tendsto_zero,
  intros n m hm,
  suffices : |∑ k in range (m - n), (-1) ^ k * a (n + k)| ≤ a n,
  { simp only [alternating_partial_sum, real.dist_eq],
    rw [abs_sub_comm, ← sum_Ico_eq_sub _ hm, sum_Ico_eq_sum_range],
    simpa [pow_add, mul_assoc, ← mul_sum, abs_mul, abs_pow] },
  rw abs_of_nonneg,
  { apply alternating_partial_sum_le_first (ha_anti.add_const_left _) (λ _, ha_nonneg _) },
  { apply alternating_partial_sum_nonneg (ha_anti.add_const_left _) (λ _, ha_nonneg _) }
end

[urkud]

You can also deduce cauchy_seq_of_le_tendsto_0' from cauchy_seq_of_le_tendsto_0.

[PatrickMassot]

If you really insist on having this variation, which I think is not a good idea, then you should add, next to cauchy_seq.add in topology/algebra/uniform_group.lean,

lemma cauchy_seq.neg {α : Type*} [uniform_space α] [add_group α] [uniform_add_group α]
  {ι : Type*} [semilattice_sup ι] {u : ι → α} (h : cauchy_seq u) : cauchy_seq (-u) :=
uniform_continuous_neg.comp_cauchy_seq h

and then prove that in terms of the previous one using:

theorem alternating_partial_sum_is_cauchy_seq'
  (ha_tendsto_zero : tendsto a at_top (𝓝 0))
  (ha_anti : antitone a)
  (ha_nonneg : ∀ n, 0 ≤ a n) :
  cauchy_seq (alternating_partial_sum' a) :=
begin
  change cauchy_seq (λ k, ∑ n in range k, (-1)^n * -(a n)),    
  simp only [sum_neg_distrib, mul_neg_eq_neg_mul_symm],
  exact (alternating_partial_sum_is_cauchy_seq ha_tendsto_zero ha_anti ha_nonneg).neg
end

[ecstatic-morse]

Thanks for the feedback. I'll open smaller PRs with the stupid lemmas that will still be necessary and then come back to this. I'm also experimenting with formalizing a more general version (Dirichlet's test).

[ecstatic-morse]

Closing in favor of #11908.