comments on FiniteMeasure user-friendliness

Stream: Polynomial Freiman-Ruzsa conjecture

[Kalle Kytölä]

Terence Tao said:

In my (now obsolete) build, notation like P[E] is automatically unfolded for some reason to (fun s ↦ ENNReal.toNNReal (↑↑↑(finiteMeasure Ω) s)) E in the infoview.

Terence Tao said:

I suspect it has something to do with the finiteMeasure class, which seems like it is held together with Lean's equivalent of duct tape

I fully agree that FiniteMeasure and ProbabilityMeasure implementations are bad at the moment, and they should definitely be fixed/improved! There is in fact some ongoing work in that direction, starting with #8375, but let me give some background to explain the duct tape.

Probability measures and finite measures were essentially my first contribution to Mathlib3; my goal was to provide basics of weak convergence / convergence in distribution. This meant that the contributions were perhaps not the most mature to start with.

Then in the porting Mathlib3 -> Mathlib4 something happened with how coercions are dealt with that I don't yet understand. In Mathlib4 we started seeing the "pretty"-printed forms such as (fun s => ENNReal.toNNReal (↑↑↑P s)) x : NNReal; see this discussion. There is a PR #8375 to start fixing the coe-handling for Measure, after which I hope one could fix it for finite measures and probability measures.

Finally, I care about making the user interface of FiniteMeasure and ProbabilityMeasure good, but there is some disagreement on what will be good for the user, especially regarding where to use Real, NNReal, and ENNReal. Some relevant discussion can be found here. I was leaning towards changing the probabilities to be real numbers, contrary to my original choice of making them NNReals. But more experienced users were not convinced of this. In my mind the best choice is still an open problem, so I have not embarked on refactors yet.

And as a comment about this PFR project, I agree with Sebastien Gouezel's comment, which advices against using FiniteMeasure and ProbabilityMeasure here, unless one needs the topology of weak convergence of measures. Using the type classes IsFiniteMeasure and IsProbabilityMeasure one gets more generally applicable statements and direct access to the Measure API.

By the way, I'm super excited about this new formalization project of yours! (And I was excited about the previous one and the insightful frequent posts about it.)

[Sebastien Gouezel]

@Kalle Kytölä , @Rémy Degenne , do you think it is finally time to wrap up some API to be able to use seamlessly measures as real-valued objects? I imagine something like

import Mathlib

open MeasureTheory Measure
open scoped NNReal

namespace MeasureTheory

variable {α : Type*} {_ : MeasurableSpace α} (μ : Measure α)

protected def Measure.real (s : Set α) : ℝ :=
  (μ s).toReal

protected def Measure.nnreal (s : Set α) : ℝ≥0 :=
  (μ s).toNNReal

variable {μ} [IsFiniteMeasure μ]

lemma measure_union_real {s t : Set α} (h : Disjoint s t) (ht : MeasurableSet t) :
    μ.real (s ∪ t) = μ.real s + μ.real t := by
  simp only [Measure.real]
  rw [measure_union h ht, ENNReal.toReal_add (measure_ne_top μ s) (measure_ne_top μ t)]

and so on. It would mean duplicating (or triplicating if we go for both real and nnreal versions) many measure lemmas, but I would guess not so many. Opinions?

[Sebastien Gouezel]

Of course, one would need some notation to hide this from the user in common probability situations. For instance like

scoped[ProbabilityTheory] notation "ℙᵣ" => MeasureTheory.MeasureSpace.volume.real

open scoped ProbabilityTheory

variable {β : Type*} [MeasureSpace β] [IsFiniteMeasure (volume : Measure β)]

example {s t : Set β} (h : Disjoint s t) (ht : MeasurableSet t) :
     ℙ (s ∪ t) = ℙ s + ℙ t :=
  measure_union h ht

example {s t : Set β} (h : Disjoint s t) (ht : MeasurableSet t) :
    ℙᵣ (s ∪ t) = ℙᵣ s + ℙᵣ t :=
  measure_union_real h ht

[Jason KY.]

Perhaps you can reuse the API for vector valued measures in this case

[Rémy Degenne]

I agree that it is time to introduce a definition for real-valued measures. I don't think we should introduce the NNReal one. Computing with NNReal is as painful as with ENNReal (or even more because we don't get summability for free) and the info that the number is nonnegative can be handled as well by the positivity tactic (if we tell it that Measure.real is nonnegative).

[Kalle Kytölä]

I am very much in favor of developing these and I agree that now is probably a good time for it. I expect I will have some time for this during the weekend.

It is currently unclear to me whether the FunLike refactor of Measure (at least) needs to happen before the duplication or triplication of the API, though.

[Kalle Kytölä]

I also feel the same way as Rémy Degenne about working with NNReal (i.e., better to avoid it!). But at least @Jireh Loreaux disagreed on that issue here.

[Sebastien Gouezel]

I also agree about avoiding NNReal. The main pitfall I can see is that when writing ℙᵣ s - ℙᵣ t you would use the badly behaved subtraction. Also, ring and friends don't work well there.

[Kalle Kytölä]

(As a small caveat, I think there are some reasons for working with NNReal-valued bounded continuous functions for weak convergence and Riesz representation theorem, because this is more seamless with lintegral. But that is irrelevant to the coercions we are discussing here, so let's maybe have any differing opinions on that elsewhere.)

[Sebastien Gouezel]

Rémy Degenne said:

I agree that it is time to introduce a definition for real-valued measures.

Do you really want to introduce a new definition of a new class of measures, or only API around the good old measures we already have as I was advocating above?

[Rémy Degenne]

I mean your Measure.real

[Floris van Doorn]

I think this is also a good idea.
Ideally I would like Measure.real to also work well with measures applied to sets with finite measure, e.g. μ (ball x r) assuming [IsFiniteMeasureOnCompacts μ]. It would be nice to have a finiteness tactic, similar to (but simpler than) the positivity tactic that can prove goals of the form μ t ≠ ⊤ and then we could have lemmas like this:

lemma measure_union_real (μ s ≠ ⊤ := by finiteness) (μ t ≠ ⊤ := by finiteness)
    (h : Disjoint s t) (ht : MeasurableSet t) :
    μ.real (s ∪ t) = μ.real s + μ.real t

[Floris van Doorn]

But maybe we should go with the simpler idea for finite measures first.

[Sebastien Gouezel]

Great idea, having a finiteness discharger like this would be awesome! If you know how to set up such a discharger in the simplest situation of finite measures (it would just apply measure_ne_top), we could start using it right away when setting up the theory, and then extend the discharger to more interesting situations.

[Floris van Doorn]

Here is a small example

import Mathlib.MeasureTheory.Measure.MeasureSpace

open MeasureTheory Measure
open scoped ENNReal

macro "finiteness" : tactic => `(tactic|apply measure_ne_top)

namespace MeasureTheory

variable {α : Type*} {_ : MeasurableSpace α} (μ : Measure α)

protected def Measure.real (s : Set α) : ℝ :=
  (μ s).toReal

variable {μ : Measure α} {s t : Set α}

lemma measure_union_real (h : Disjoint s t) (ht : MeasurableSet t)
  (hs : μ s ≠ ∞ := by finiteness) (h2t : μ t ≠ ∞ := by finiteness)  :
    μ.real (s ∪ t) = μ.real s + μ.real t := by
  simp only [Measure.real]
  rw [measure_union h ht, ENNReal.toReal_add hs h2t]

example [IsProbabilityMeasure μ] (h : Disjoint s t) (ht : MeasurableSet t) :
    μ.real (s ∪ t) = μ.real s + μ.real t :=
  measure_union_real h ht

end MeasureTheory

[Sebastien Gouezel]

Let me try to cook up a basic API using this. I propose to do it in the FPR project, to see what we need and add it progressively to the file. Of course, the goal in the end is to move it back to mathlib once things have stabilized.

[Heather Macbeth]

I think a finiteness tactic could be built quickly with aesop (with backtracking turned off). The reason positivity isn't built withaesop is the slightly nontrivial interaction of < and <= proofs of subexpressions, but there is no such issue for finiteness.

[Jason KY.]

Jason KY. said:

Perhaps you can reuse the API for vector valued measures in this case

To elaborate on this, you can define Measure.real as a signed measure (which already exist in mathlib) with a positivity condition. In this case, all the lemmas for vector measure will still apply and there is also existing API for transforming between measures and signed measures.

[Kalle Kytölä]

I think I'd prefer to have a mechanism to talk about the real values of ordinary measures under suitable hypotheses (finite measure, probability measure, or perhaps even locally finite measure of some kind like in Floris van Doorn's comment above --- this last one is particularly problematic for vector measures). Then all other objects such as FiniteMeasure and ProbabilityMeasure can access the real-valuedness API of Measure. To me this is the most direct advantage of Sebastien Gouezel's proposed approach with Measure.real etc.

[Sebastien Gouezel]

The basic API is now available at https://github.com/teorth/pfr/pull/14. Comments welcome!

[Kalle Kytölä]

This looks great to me, and honestly I'd love to have it in Mathlib soon!

[Heather Macbeth]

Heather Macbeth said:

I think a finiteness tactic could be built quickly with aesop (with backtracking turned off).

Prototype version in https://github.com/teorth/pfr/pull/20.

[Heather Macbeth]

Here are some things it can do:

example : (1:ℝ≥0∞) < ∞ := by finiteness
example : (3:ℝ≥0∞) ≠ ∞ := by finiteness

example (a : ℝ) (b : ℕ) : ENNReal.ofReal a + b < ∞ := by finiteness

example {a : ℝ≥0∞} (ha : a ≠ ∞) : a + 3 < ∞ := by finiteness
example {a : ℝ≥0∞} (ha : a < ∞) : a + 3 < ∞ := by finiteness

example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ∞ := by finiteness

[Heather Macbeth]

That is in fact the entirety of the current test set :) please test more ...

[Bhavik Mehta]

This looks very useful, but I think it would be also nice to have a tactic which can prove that Sets are finite (to improve the auto-param that's used a lot in Nat.card, for example). And that one could also be called finiteness! It's probably not sensible for this one to do both, so how should we resolve the naming?

[Kevin Buzzard]

set_finiteness?

[Scott Morrison]

It's a pretty cheap dispatch to just look at the goal and decide whether to call numeric_finiteness or set_finiteness under the hood.

[Kalle Kytölä]

Contrary to what I said before, I think there is a place for FiniteMeasure in PFR after all: a small part of the argument is topological (continuity of the entropy-like quantities and compactness for the existence of minimizers) and docs#MeasureTheory.FiniteMeasure has a topology instance, which for finite types (with discrete topology) coincides with the natural topology. I think rather than introducing any other topology, it would be good to use the exsisting one. I have intended (for a long time) to include this in the API of weak convergence in finite spaces anyway.

I still think it is good to do most other parts in just Measure.

Here is a quick and dirty "continuity of the singleton measures" assuming [DiscreteTopology Ω], when FiniteMeasure Ω has the topology of weak convergence. That should easily give continuity of the entropy-like quantities with Rémy Degenne's definitions. I would next prove that with [Fintype Ω] we have that FiniteMeasure Ω is homeomorphic to Ω → ℝ≥0, and compactness should then be easy.

import Mathlib.MeasureTheory.Measure.Portmanteau
import Mathlib.MeasureTheory.Measure.Count
import Mathlib.Tactic
import PFR.MeasureReal

open MeasureTheory Topology Metric Filter Set ENNReal NNReal

open scoped Topology ENNReal NNReal BoundedContinuousFunction

variable {ι : Type _} {Ω : Type _} --[Fintype Ω]
variable [MeasurableSpace Ω] [MeasurableSingletonClass Ω]
variable [TopologicalSpace Ω] [DiscreteTopology Ω] [OpensMeasurableSpace Ω]

--#check IsolatedPoint -- Does not exist. What is the Mathlib-spelling?

section auxiliary

lemma continuous_indicator_const {α β : Type*} [TopologicalSpace α]
    [Zero β] [TopologicalSpace β] {b : β} {s : Set α}
    (s_open : IsOpen s) (s_closed : IsClosed s) :
    Continuous (indicator s (fun _ ↦ b)) := by
  rw [continuous_def]
  intro t _
  classical
  have := @indicator_const_preimage_eq_union α β _ s t b _ _
  rw [this]
  apply IsOpen.union
  · by_cases ht : b ∈ t
    · simp only [ht, ite_true, s_open]
    · simp only [ht, ite_false, isOpen_empty]
  · by_cases ht : 0 ∈ t
    · simp only [ht, ite_true, isOpen_compl_iff, s_closed]
    · simp only [ht, ite_false, isOpen_empty]

lemma continuous_indicator_singleton {α : Type*} [TopologicalSpace α] [T1Space α]
    {a : α} (ha : IsOpen {a}) :
    Continuous (indicator {a} (fun _ ↦ (1 : ℝ≥0))) :=
  continuous_indicator_const ha (T1Space.t1 a)

lemma continuous_integral_finiteMeasure
    {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (f : α →ᵇ ℝ) :
    Continuous (fun (μ : FiniteMeasure α) ↦ ∫ x, f x ∂μ) := by
  apply continuous_iff_continuousAt.mpr
  intro μ
  apply continuousAt_of_tendsto_nhds
  exact FiniteMeasure.tendsto_iff_forall_integral_tendsto.mp tendsto_id f

noncomputable def indicatorBCF {α : Type*} [TopologicalSpace α]
    {s : Set α} (s_open : IsOpen s) (s_closed : IsClosed s) :
    BoundedContinuousFunction α ℝ where
      toFun := s.indicator (fun _ ↦ (1 : ℝ))
      continuous_toFun := continuous_indicator_const s_open s_closed
      map_bounded' := by
        use 1
        intro x y
        by_cases hx : x ∈ s
        · by_cases hy : y ∈ s
          · simp only [hx, hy, indicator_of_mem, dist_self, zero_le_one]
          · simp only [hx, hy, indicator_of_mem, not_false_eq_true, indicator_of_not_mem,
                       dist_zero_right, norm_one, le_refl]
        · by_cases hy : y ∈ s
          · simp only [hx, hy, not_false_eq_true, indicator_of_not_mem, indicator_of_mem,
                       dist_zero_left, norm_one, le_refl]
          · simp only [hx, hy, not_false_eq_true, indicator_of_not_mem, dist_self, zero_le_one]

@[simp] lemma indicatorBCF_apply  {α : Type*} [TopologicalSpace α]
    {s : Set α} (s_open : IsOpen s) (s_closed : IsClosed s) (x : α) :
    indicatorBCF s_open s_closed x = s.indicator (fun _ ↦ (1 : ℝ)) x := rfl

lemma lintegral_indicatorBCF {α : Type*} [TopologicalSpace α] [MeasurableSpace α] (μ : Measure α)
    {s : Set α} (s_open : IsOpen s) (s_closed : IsClosed s) (s_mble : MeasurableSet s) :
    ∫⁻ x, ENNReal.ofReal (indicatorBCF s_open s_closed x) ∂μ = μ s := by
  convert lintegral_indicator_one s_mble
  rename_i x
  by_cases hx : x ∈ s <;> simp [hx]

lemma integral_indicatorBCF {α : Type*} [TopologicalSpace α] [MeasurableSpace α] (μ : Measure α)
    {s : Set α} (s_open : IsOpen s) (s_closed : IsClosed s) (s_mble : MeasurableSet s) :
    ∫ x, (indicatorBCF s_open s_closed x) ∂μ = (μ s).toReal := by
  exact integral_indicator_one s_mble

/-- The measure of any connected component depends continuously on the `FiniteMeasure`. -/
lemma continuous_finiteMeasure_apply_of_isOpen_of_isClosed
    {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
    {s : Set α} (s_open : IsOpen s) (s_closed : IsClosed s) :
    Continuous (fun (μ : FiniteMeasure α) ↦ (μ : Measure α).real s) := by
  convert continuous_integral_finiteMeasure (indicatorBCF s_open s_closed)
  have s_mble : MeasurableSet s := IsOpen.measurableSet s_open
  rw [integral_indicatorBCF _ s_open s_closed s_mble]
  rfl

end auxiliary -- section

section pmf

namespace FiniteMeasure

def pmf (μ : FiniteMeasure Ω) (ω : Ω) : ℝ := (μ : Measure Ω).real {ω}

/-
Q: Why doesn't the spelling `μ.pmf` work?

invalid field 'pmf', the environment does not contain 'Subtype.pmf'
  μ
has type
  { μ // IsFiniteMeasure μ }
-/
lemma continuous_pmf_apply (ω : Ω) :
    Continuous (fun (μ : FiniteMeasure Ω) ↦ FiniteMeasure.pmf μ ω) :=
  continuous_finiteMeasure_apply_of_isOpen_of_isClosed (isOpen_discrete _) (T1Space.t1 _)

end FiniteMeasure -- namespace

end pmf --section

[Kalle Kytölä]

Can I push to the repo? I'd like to work on these continuity / compactness aspects (although not before today evening), I have intended to include the API for the topology of weak convergence in finite spaces anyway.

[Rémy Degenne]

You should fork the repo, work on your fork, then make a PR

[Sebastien Gouezel]

I have started to work on the compactness of the space of probability measures on a finite space (it's true more generally on compact spaces, but one would need Riesz representation theorem, but here there is a shortcut that it's equivalent to a standard simplex, and the equivalence is good to have anyway). To coordinate a little bit, would you agree to let me complete the proof of compactness, while you do the continuity of entropy and of the tau functional?

[Sebastien Gouezel]

I have PRed the compactness at https://github.com/teorth/pfr/pull/33. It relies on a sorried result that values of a probability measure at a point depend continuously on the measure, a result which is in your post above, so when you PR you will as well complete the compactness proof!

[Kalle Kytölä]

Thanks! I will clean up a bit and try to fork & PR the continuity part.

By the way, I'd be really happy if your MeasureReal.lean was PR'd to Mathlib. I'd like to fix the CoeFun of FiniteMeasure to a Funlike (I hope this would fix the pretty-printing issue) using your Measure.real. Since this replaces an existing coercion, I think this refactor needs to happen directly in Mathlib. I have read at least one version of your code, so could do a quick review (although I'm clearly all the time slower than anyone else here; the for example the whole compactness thing happened while I was away from my computer for the day).

[Bhavik Mehta]

Scott Morrison said:

It's a pretty cheap dispatch to just look at the goal and decide whether to call numeric_finiteness or set_finiteness under the hood.

That's true, but it feels to me like it goes against modularity of tactics. But I'd be happy to have either, ultimately this is the kind of proof I'd never like to write myself in Lean!