Vitali's convergence theorem

Stream: maths

[Igor Khavkine]

Greetings! :wave: The version of Vitali's convergence theorem in Mathlib docs#MeasureTheory.tendstoInMeasure_iff_tendsto_Lp requires the IsFiniteMeasure hypothesis. The result of course holds even if the underlying measure space has infinite volume, requiring instead the additional hypothesis that the converging functions are "uniformly tight".

I've formalized the proof of this more general version. I'm posting it below. It'd be nice to include it in Mathlib eventually. But since it is my first experience with Lean (or any proof assistant), I'd be happy to hear any comments about doing things more inline with best practices. I've left XXX marks in the code where I had some specific questions or issues. If it's clear that the code could be integrated into Mathlib, a pointer to instructions on how to make a pull request would be welcome.

A comment about my experience. One of the biggest headaches was dealing with routine ENNReal arithmetic. Neither linarith nor field_simp nor simp were of any help. It'd be nice to have extra assistance here, since I've noticed that ENNReal is used everywhere in measure theory.

[Igor Khavkine]

Can't post it directly (too long). I'll set up a small git repository and post the link to it in a bit.

[Ruben Van de Velde]

Pointer: https://leanprover-community.github.io/contribute/index.html ; you'll need to ask for push access to the main repository if you don't have it yet

[Igor Khavkine]

Here it is (about 550 lines): https://github.com/igorkhavkine/VitaliConvergence/blob/main/VitaliConvergence.lean

[Ruben Van de Velde]

AEStronglyMeasurable.ennnorm returning AEMeasurable rather than AEStronglyMeasurable seems odd to me as well; cc @Sebastien Gouezel who added it in !3#12985

[Sebastien Gouezel]

It is the reasonable and useful statement: for ENNReal-valued functions, the assumption one uses all the time for the Lebesgue integral is AEMeasurable, while AEStronglyMeasurable is more relevant for Bochner integration, i.e., for functions taking values in a vector space. This should probably be more properly explained in the docstring!

[Igor Khavkine]

(AE)StronglyMeasurable is used everywhere around Lp spaces, so I naturally followed that trend. I updated the core lintegral_indicator_compl_le lemma to use only AEMeasurable.

[Igor Khavkine]

Still it would make more sense to me to get AEMeasurable from hstrongmeasfunc.ennnorm.aemeasurable rather that straight from hstrongmeasfunc.ennnorm. Afterall hstrongmeasfunc.nnnorm.aemeasurable does the expected thing.

[Igor Khavkine]

Also, about consistency. I've noticed that in different parts under MeasureTheory a.e. convergence when referred to in theorem names sometimes is written as ae_tendsto and sometimes tendsto_ae. It's about 50%/50% as far as I can tell. Would it make sense to standardize that?

[Igor Khavkine]

Another thing I found confusing. What is the right way to attach an instance of IsFiniteMeasure μto a measure space? It is an implicit argument that is expected to be synthesized when calling tendsto_Lp_of_tendsto_ae_of_meas. What is the purpose of wrapping a proof of μ univ < ∞inside IsFiniteMeasure μ or more generally Fact (...)?

[Ruben Van de Velde]

Possibly so you don't have to pass the hypothesis manually every time

[Igor Khavkine]

What is the underlying Lean mechanism here? I guess I just don't understand what's different between arguments [IsFiniteMeasure μ] or [μ univ < ∞] or just leaving a _ in place of an argument when invoking a theorem.

[Ruben Van de Velde]

The terms you're looking for are "type class" or "instance argument"

[Kevin Buzzard]

Note that [μ univ < ∞] isn't allowed (i.e. won't work) because < is a structure but not a class.

[Sebastien Gouezel]

Igor Khavkine said:

Still it would make more sense to me to get AEMeasurable from hstrongmeasfunc.ennnorm.aemeasurable rather that straight from hstrongmeasfunc.ennnorm. Afterall hstrongmeasfunc.nnnorm.aemeasurable does the expected thing.

Indeed the first version I had was like that, with hstrongmeasfunc.ennnorm.aemeasurable. Except I realized later that all uses of AEStronglyMeasurable.ennnorm were of this form (not one single exception!), composing with .aemeasurable aferwards. So I switched to the version giving the aemeasurable conclusion, since it's the one which is really needed.

[Igor Khavkine]

Sebastien Gouezel said:

Igor Khavkine said:

Still it would make more sense to me to get AEMeasurable from hstrongmeasfunc.ennnorm.aemeasurable rather that straight from hstrongmeasfunc.ennnorm. Afterall hstrongmeasfunc.nnnorm.aemeasurable does the expected thing.

Indeed the first version I had was like that, with hstrongmeasfunc.ennnorm.aemeasurable. Except I realized later that all uses of AEStronglyMeasurable.ennnorm were of this form (not one single exception!), composing with .aemeasurable aferwards. So I switched to the version giving the aemeasurable conclusion, since it's the one which is really needed.

I understand the logic. I can only offer the perspective of a casual user. And from that perspective this choice looks like Unexpected Behavior (TM).

[Igor Khavkine]

I've now looked up some basics about typeclasses. Thanks for the hints about them! In terms of saving on typing, it seems to me that's exactly what coercions are for. Indeed, there are canonical implications in the StronglyMeasurable, Measurable, AEStronglyMeasurable and AEMeasurable hierarchy. I see no reason why they couldn't be coerced using the usual Mathlib mechanisms.

[Igor Khavkine]

Here's sample code for doing exactly that:

import Mathlib

open Classical Set Filter Topology MeasureTheory NNReal ENNReal

namespace MeasureTheory.AEStronglyMeasurable


variable {α β ι : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
variable {f : α → β}


attribute [coe] StronglyMeasurable.measurable
instance instCoeStronglyMeasurable_toMeasurable [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  : Coe (StronglyMeasurable f) (Measurable f) where
  coe h := h.measurable

variable {μ : Measure α}

attribute [coe] StronglyMeasurable.aestronglyMeasurable
instance instCoeStronglyMeasurable_toAEStronglyMeasurable [TopologicalSpace β]
  : Coe (StronglyMeasurable f) (AEStronglyMeasurable f μ) where
  coe h := h.aestronglyMeasurable

attribute [coe] AEStronglyMeasurable.aemeasurable
instance instCoeAEStronglyMeasurable_toAEMeasurable [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  : Coe (AEStronglyMeasurable f μ) (AEMeasurable f μ) where
  coe h := h.aemeasurable

attribute [coe] Measurable.aemeasurable
instance instCoeMeasurable_toAEMeasurable
  : Coe (Measurable f) (AEMeasurable f μ) where
  coe h := h.aemeasurable

-- fails: Why can't it synthesize `μ` for `AEMeasurable f _`, even though `μ` appears in `hf`?
example [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  (hf : AEStronglyMeasurable f μ) : AEMeasurable f := hf

-- works! uses the new coercions
example [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  (hf : StronglyMeasurable f) : AEMeasurable f μ := (hf : AEStronglyMeasurable f μ)
example [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  (hf : StronglyMeasurable f) : AEMeasurable f μ := (hf : Measurable f)
example [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  (hf : AEStronglyMeasurable f μ) : AEMeasurable f μ := hf
example [TopologicalSpace β] [BorelSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  (hf : Measurable f) : AEMeasurable f μ := hf

-- works! with β = ℝ≥0∞
example (f : α → ℝ≥0∞) (hf : AEStronglyMeasurable f μ) : AEMeasurable f μ := hf

-- works, but `hf.ennnorm` by current convention is already `AEMeasurable`
example (f : α → β) [SeminormedAddCommGroup β]
  (hf : AEStronglyMeasurable f μ) : AEMeasurable (fun a ↦ (‖f a‖₊ : ℝ≥0∞)) μ
  := hf.ennnorm

@[measurability]
protected theorem ennnorm_aestronglyMeasurable {β : Type*} [SeminormedAddCommGroup β] {f : α → β}
    (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun a => (‖f a‖₊ : ℝ≥0∞)) μ :=
  (ENNReal.continuous_coe.comp_aestronglyMeasurable hf.nnnorm)

-- works! this uses coercion of `AEStronglyMeasurable` to `AEMeasurable`
example (f : α → β) [SeminormedAddCommGroup β]
  (hf : AEStronglyMeasurable f μ) : AEMeasurable (fun a ↦ (‖f a‖₊ : ℝ≥0∞)) μ
  := hf.ennnorm_aestronglyMeasurable

end MeasureTheory.AEStronglyMeasurable

[Igor Khavkine]

The last example shows what I think would be expected behavior by a casual user (who happens to be aware of coercions).

[Igor Khavkine]

OK, I've managed to package my code as a branch (vitali_convergence_update) on a personal fork of Mathlib (see the last 4 commits there).

I'm happy to submit a Pull Request for review. If it makes anyone's life easier, I could just as easily add this branch to the main Mathlib repository and make a PR that way. In that case I believe I should ask someone for write access (@Sebastien Gouezel @Scott Morrison sorry if I'm pinging the wrong persons)? As far as a self-introduction, please see:

https://users.math.cas.cz/~khavkine/

[Scott Morrison]

@Igor Khavkine, invitation sent!