Tannery's theorem

Stream: Is there code for X?

[Oskar Goldhahn]

Is there code for Tannery's theorem or something like it?

I'm indexing over an arbitrary type in the sum and taking the limit in the extended positive reals.

[Oskar Goldhahn]

I'm working in Lean4

[Riccardo Brasca]

If you are referring to this, we have docs#MeasureTheory.tendsto_integral_of_dominated_convergence that is a generalization

[Oskar Goldhahn]

I saw that, but I'm struggling to get it in the form I need.

[Oskar Goldhahn]

The amount of measure theory I have to wade through here makes it challenging

[David Loeffler]

Something like this, maybe?

import Mathlib

open Filter Topology MeasureTheory

/-- Auxiliary lemma to translate integrability statements into summability -/
lemma integrable_count_iff {𝓚 G : Type*} [Countable 𝓚] [NormedAddCommGroup G] [NormedSpace ℝ G]
    [CompleteSpace G] [SecondCountableTopology G] {f : 𝓚 → G} :
    Integrable f (@Measure.count _ ⊤) ↔ Summable (fun k ↦ ‖f k‖) := by
  letI : MeasurableSpace G := borel G
  haveI : BorelSpace G := ⟨rfl⟩
  letI : MeasurableSpace 𝓚 := ⊤
  simp_rw [Integrable, eq_true_intro (MeasurableSpace.Top.measurable f).aestronglyMeasurable,
    true_and, HasFiniteIntegral, lintegral_count, lt_top_iff_ne_top,
    ENNReal.tsum_coe_ne_top_iff_summable, ← NNReal.summable_coe, coe_nnnorm]

/-- **Tannery's theorem**: countable sums commutes with limits when the norm of the summand is uniformly
bounded by a summable function.

(This is the special case of the Lebesgue dominated convergence
theorem for the counting measure on a discrete countable set.) -/
lemma tendsto_tsum_of_dominated {𝓚 G : Type*} [Countable 𝓚]
   [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] [SecondCountableTopology G]
    {a : 𝓚 → ℕ → G} {b : 𝓚 → G} {bound : 𝓚 → ℝ} (h_sum : Summable bound)
    (hab : ∀ k, Tendsto (a k) atTop (𝓝 (b k))) (h_bound : ∀ k n, ‖a k n‖ ≤ bound k) :
    Tendsto (fun n ↦ ∑' k, a k n : ℕ → G) atTop (𝓝 (tsum b)) := by
  -- choose measure space structures
  letI : MeasurableSpace G := borel G
  haveI : BorelSpace G := ⟨rfl⟩
  letI : MeasurableSpace 𝓚 := ⊤
  letI : MeasureSpace 𝓚 := ⟨Measure.count⟩
  -- set up hypotheses for dominated convergence
  have bound_int : Integrable bound
  · simpa only [integrable_count_iff] using h_sum.norm
  have b_int : Summable (fun k ↦ ‖b k‖)
  · refine h_sum.of_norm_bounded _ (fun k ↦ ?_)
    simp_rw [norm_norm]
    exact le_of_tendsto ((continuous_norm.tendsto _).comp (hab k))
      (eventually_of_forall (h_bound k))
  -- apply dominated convergence
  have DC := tendsto_integral_of_dominated_convergence _
    (fun _ ↦ (MeasurableSpace.Top.measurable _).aestronglyMeasurable)
    bound_int
    (fun n ↦ eventually_of_forall (Function.swap h_bound n))
    (eventually_of_forall hab)
  -- massage integrals back to sums in the result
  simp_rw [integral_countable' (integrable_count_iff.mpr b_int),
    Measure.count_singleton, ENNReal.one_toReal, one_smul] at DC
  convert DC using 2 with n
  rw [integral_countable']
  · simp [Measure.count_singleton]
  · rw [integrable_count_iff]
    refine h_sum.of_norm_bounded _ ?_
    simpa only [norm_norm] using (fun k ↦ h_bound k n)

[Oskar Goldhahn]

That's great, thanks a lot!

It seems to me like it should be possible to get rid of the countability assumption because summability of the bound implies that a has countable support. Am I wrong?

[David Loeffler]

Oskar Goldhahn said:

That's great, thanks a lot!

It seems to me like it should be possible to get rid of the countability assumption because summability of the bound implies that a has countable support. Am I wrong?

Sounds like an exercise for the reader :smile:

[Oskar Goldhahn]

I'll give it a try.

Thanks again!

[Oskar Goldhahn]

I managed to get rid of the countability as well. It seems to me like countability is also unneeded in some of the adjacent theorems, such as integral_countable'.

Does it make sense to try to get this added to Mathlib?

Here's the resulting code, which can surely be shortened (I'm comfortable with proof assistants in general but not used to Lean specifically):

import Mathlib
open Filter Topology MeasureTheory

/-- Auxiliary lemma to translate integrability statements into summability -/
lemma integrable_count_iff {𝓚 G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
    [SecondCountableTopology G] {f : 𝓚 → G} :
    Integrable f (@Measure.count _ ⊤) ↔ Summable (fun k ↦ ‖f k‖) := by
  letI : MeasurableSpace G := borel G
  haveI : BorelSpace G := ⟨rfl⟩
  letI : MeasurableSpace 𝓚 := ⊤
  simp_rw [Integrable, eq_true_intro (MeasurableSpace.Top.measurable f).aestronglyMeasurable,
    true_and, HasFiniteIntegral, lintegral_count, lt_top_iff_ne_top,
    ENNReal.tsum_coe_ne_top_iff_summable, ← NNReal.summable_coe, coe_nnnorm]

/-- **Tannery's theorem**: countable sums commutes with limits when the norm of the summand is uniformly
bounded by a summable function.

(This is the special case of the Lebesgue dominated convergence
theorem for the counting measure on a discrete countable set.) -/
lemma tendsto_tsum_of_dominated {𝓚 G : Type*}
   [NormedAddCommGroup G] [NormedSpace ℝ G] [CompleteSpace G] [SecondCountableTopology G]
    {a : 𝓚 → ℕ → G} {b : 𝓚 → G} {bound : 𝓚 → ℝ} (h_sum : Summable bound)
    (hab : ∀ k, Tendsto (a k) atTop (𝓝 (b k))) (h_bound : ∀ k n, ‖a k n‖ ≤ bound k) :
    Tendsto (fun n ↦ ∑' k, a k n : ℕ → G) atTop (𝓝 (tsum b)) := by
  -- handle uncountable 𝓚
  have bound_supp_sub_a_supp n k : bound k = 0 → a k n = 0
  · intros bound_eq_zero
    suffices : ‖a k n‖ ≤ 0
    · simpa
    rw [←bound_eq_zero]
    exact h_bound k n
  have count_a_supp : Countable bound.support
  · apply Set.Countable.to_subtype
    apply Summable.countable_support h_sum
  let b' (k: bound.support) : G := b k
  let bound' (k: bound.support) : ℝ := bound k
  let h_sum': Summable bound'
  · match h_sum with
    | ⟨x, p⟩ => (
      exists x
      rw [←hasSum_subtype_support] at p
      have bound_eq : bound' = bound ∘ Subtype.val := rfl
      rw [bound_eq]
      exact p
    )
  let hab' (k : bound.support): Tendsto (a k) atTop (𝓝 (b k)) := hab k
  let h_bound' (k : bound.support) (n : ℕ) : ‖a k n‖ ≤ bound k := h_bound k n
  -- choose measure space structures
  letI : MeasurableSpace G := borel G
  haveI : BorelSpace G := ⟨rfl⟩
  letI : MeasurableSpace bound.support := ⊤
  letI : MeasureSpace bound.support := ⟨Measure.count⟩
  -- set up hypotheses for dominated convergence
  have bound_int : Integrable bound'
  · simpa only [integrable_count_iff] using h_sum'.norm
  have b_int : Summable (fun k ↦ ‖b' k‖)
  · refine h_sum'.of_norm_bounded _ (fun k ↦ ?_)
    simp_rw [norm_norm]
    exact le_of_tendsto ((continuous_norm.tendsto _).comp (hab k))
      (eventually_of_forall (h_bound k))
  -- apply dominated convergence
  have DC := tendsto_integral_of_dominated_convergence _
    (fun _ ↦ (MeasurableSpace.Top.measurable _).aestronglyMeasurable)
    bound_int
    (fun n ↦ eventually_of_forall (Function.swap h_bound' n))
    (eventually_of_forall hab')
  -- massage integrals back to sums in the result
  simp_rw [integral_countable' (integrable_count_iff.mpr b_int),
    Measure.count_singleton, ENNReal.one_toReal, one_smul] at DC
  convert DC using 2 with n
  rw [integral_countable']
  · simp [Measure.count_singleton]
    rw [←tsum_subtype_eq_of_support_subset]
    simp
    intros k
    contrapose
    simp
    intros H
    apply bound_supp_sub_a_supp
    rw [H]
  · rw [integrable_count_iff]
    refine h_sum'.of_norm_bounded _ ?_
    simpa only [norm_norm] using (fun k ↦ h_bound' k n)
  · simp_all
    apply Eq.symm
    rw [tsum_subtype_eq_of_support_subset]
    simp
    intros k
    contrapose
    simp
    intros bound_eq0
    have tendsto0 : Tendsto (a ↑k) atTop (𝓝 (0))
    · have ak_const : a k = fun n => 0
      · funext n
        apply bound_supp_sub_a_supp
        exact bound_eq0
      rw [ak_const]
      exact tendsto_const_nhds
    apply tendsto_nhds_unique (hab k) tendsto0

[David Loeffler]

Sorry, I only just saw this. I think this would be a nice addition to mathlib; but the result is kind of non-optimal, because it only applies when the "limit" variable n is varying over the natural numbers.

I think the result is actually true with all the limits along atTop ℕ replaced by limits along an arbitrary filter. That would be an awesome thing to have in mathlib, but would need a different proof.