Uncountable sum diverges

Stream: Is there code for X?

[Praneeth Kolichala]

For example, the uncountable sum of real numbers diverges. I have a proof, but it is long and might duplicate lemmas that already exist, since I'm still getting familiar with this part of mathlib:

Code

import data.set.basic
import algebra.big_operators.basic
import analysis.normed.group.infinite_sum

open_locale big_operators topological_space

section
variables {γ : Type*} [topological_space γ] [sequential_space γ]

/-- A non isolated point `x` in a sequential space has a sequence converging to it -/
lemma exists_seq_of_not_isolated (x : γ) [filter.ne_bot (𝓝[≠] x)] :
  ∃ seq : ℕ → γ, (∀ n, seq n ≠ x) ∧ filter.tendsto seq filter.at_top (𝓝 x) :=
begin
  have : ∀ (seq : ℕ → γ), (∀ n, seq n ≠ x) ↔ (∀ n, seq n ∈ {x}ᶜ),
  { intro,
  /- Doesn't work for some reason? -/
  --simp_rw set.mem_compl_singleton_iff,
  split, { intros, rw set.mem_compl_singleton_iff, tauto }, simp },
  simp_rw this,
  rw [← mem_closure_iff_seq_limit, closure_compl_singleton],
  trivial,
end

end

section
variables {α : Type*} {β : Type*} [linear_ordered_add_comm_group β]
  [topological_space β] [order_closed_topology β]

/-- If a function tends to `0`, then it is eventually less than every `b > 0` -/
lemma lt_abs_of_tendsto_zero {f : α → β} {s : filter α} (hs : filter.tendsto f s (𝓝 0))
  (b : β) (hb : 0 < b) : ∀ᶠ n in s, |f n| < b :=
begin
  simp_rw abs_lt,
  simp only [filter.eventually_and], split,
  { apply eventually_gt_of_tendsto_gt (_ : -b < 0) hs, rw neg_lt_zero, exact hb, },
  exact eventually_lt_of_tendsto_lt hb hs,
end

/-- Mild generalization of `finite_of_summable_const` -/
lemma finite_of_summable_geq_const [archimedean β] {f : α → β}
  (hf : summable f) {b : β} (hb : 0 < b) (f_geq : ∀ a, b ≤ f a) :
  nonempty (fintype α) :=
begin
  have H : ∀ s : finset α, s.card • b ≤ ∑' a : α, f a,
  { intros s,
    have := (finset.sum_le_sum (λ i (hi : i ∈ s), f_geq i)).trans (sum_le_has_sum s (λ a ha, hb.le.trans (f_geq a)) hf.has_sum),
    simpa, },
  obtain ⟨n, hn⟩ := archimedean.arch (∑' a : α, f a) hb,
  have : ∀ s : finset α, s.card ≤ n := λ s, (nsmul_le_nsmul_iff hb).mp ((H s).trans hn),
  exact nonempty.intro (fintype_of_finset_card_le n this),
end

end

section
variables {α : Type*} {β : Type*} [linear_ordered_add_comm_group β] [archimedean β]
  [uniform_space β] [order_closed_topology β]
  [uniform_add_group β] [complete_space β] {f : α → β}
  (hf : summable f)

include hf
lemma finite_of_summable_geq_const' {b : β} (hb : 0 < b) :
  set.finite {x : α | b ≤ f x} :=
begin
  rw set.finite_def,
  exact finite_of_summable_geq_const (summable.subtype hf {x | b ≤ f x}) hb subtype.property,
end

theorem countable_of_summable [sequential_space β] [filter.ne_bot (𝓝[≠] (0 : β))] : (function.support f).countable :=
begin
  obtain ⟨seq, ⟨nonzero, limit⟩⟩ := exists_seq_of_not_isolated (0 : β),
  have : (⋃ n, { x : α | |seq n| < |f x| }) = function.support f,
  { ext x, split,
    { simp only [set.mem_Union, set.mem_set_of_eq, function.mem_support, ne.def, forall_exists_index],
      intros n hn fz, rw [fz, abs_zero] at hn, exact not_lt_of_le (abs_nonneg (seq n)) hn, },
    intro hf₂,
    have := lt_abs_of_tendsto_zero limit (|f x|) (abs_pos.mpr hf₂),
    simp only [filter.eventually_at_top] at this,
    obtain ⟨N, hN⟩ := this, specialize hN N le_rfl,
    simp only [set.mem_Union],
    use N, exact hN },
  rw ← this,
  apply set.countable_Union,
  intro a, apply set.finite.countable,
  suffices : {x : α | |seq a| ≤ |f x|}.finite,
  { exact set.finite.subset this (λ x hx, le_of_lt hx) },
  apply finite_of_summable_geq_const', { rw summable_abs_iff, exact hf },
  rw abs_pos, exact nonzero a,
end

end

Some of these lemmas seem like they should be in the library already, but I couldn't find them using library_search.

Also, my feeling is that some of the typeclass constraints are unnecessary. I tried to essentially port my proof from the one in real numbers, but this might not be the most efficient way to do it in general.

[Yury G. Kudryashov]

Here is an idea of a simpler proof. The main lemma is

open set filter
lemma filter.tendsto.countable_set_of_ne {α X : Type*} [topological_space X] [t1_space X]
  {f : α → X} {b : X} (hf : tendsto f cofinite (𝓝 b)) [is_countably_generated (𝓝 b)] :
  countable {a | f a ≠ b}

[Yury G. Kudryashov]

Your statement follows from this lemma and docs#summable.tendsto_cofinite_zero

[Yury G. Kudryashov]

To prove this lemma, choose a specific countable basis of nhds of b (e.g., using docs#filter.exists_antitone_basis). The preimage of each neighborhood is cofinite, hence the complement of the preimage of their intersection is countable. Due to docs#bInter_basis_nhds, this intersection is {b} and you get the desired statement.