Are discrete measures determined by their points?

Stream: maths

[Bolton Bailey]

After some discussions about PMF #mathlib4 > PMF Refactor: FunLike vs Definition Change , I am curious about the DiscreteMeasurableSpace API . Can someone with a good intuition for these things tell me, is docs#MeasureTheory.Measure.map_eq_sum true if we replace the typeclass assumption with DiscreteMeasurableSpace? If not, is there a counterexample I can think about?

[Bolton Bailey]

Also, what about

theorem DiscreteMeasurableSpace.ext_of_singleton [DiscreteMeasurableSpace α] {μ ν : Measure α}
    (h : ∀ a, μ {a} = ν {a}) : μ = ν := by sorry

[James E Hanson]

Your second statement is false if there is a measurable cardinal, the existence of which is independent of the type theory of Lean. Specifically, you can have a $\{0,1\}$-valued measure $\mu$ on the full power set of a given set $X$ such that $\mu(X) = 1$ but $\mu(\{x\}) = 0$ for every $x \in X$.

[Aaron Liu]

surely we don't need a measurable cardinal though?

[Aaron Liu]

we can set $\mu(X) = \infty$ instead, right?

[Etienne Marion]

Infinity times Lebesgue measure can be extended to all sets no?

[James E Hanson]

Aaron Liu said:

we can set $\mu(X) = \infty$ instead, right?

Oh sure, but if we add the assumption that $\mu(X) < \infty$, then I believe the statement is equivalent to the non-existence of a real-valued measurable cardinal.

[Aaron Liu]

here we go

import Mathlib

open MeasureTheory

variable {α : Type*} [MeasurableSpace α] in
theorem DiscreteMeasurableSpace.ext_of_singleton [DiscreteMeasurableSpace α] {μ ν : Measure α}
    (h : ∀ a, μ {a} = ν {a}) : μ = ν := by sorry

example : False := by
  classical
  obtain ⟨α, hα⟩ : ∃ α : Type, Uncountable α := ⟨Real, inferInstance⟩
  let : MeasurableSpace α := ⊤
  let μ : Measure α := {
    measureOf s := if s.Countable then 0 else ⊤
    empty := by simp
    mono h := by
      split_ifs with h₁ h₂ h₂
      · rfl
      · apply le_top
      · exact (h₁ (h₂.mono h)).elim
      · rfl
    iUnion_nat seq _ := by
      rw [Set.countable_iUnion_iff]
      split_ifs with h
      · apply zero_le
      · rw [not_forall] at h
        obtain ⟨i, hi⟩ := h
        refine le_trans ?_ (ENNReal.summable.le_tsum' i)
        simp [hi]
    m_iUnion seq _ _ := by
      change ite .. = _
      rw [Set.countable_iUnion_iff]
      by_cases h : ∀ (i : ℕ), (seq i).Countable
      · rw [if_pos h]
        conv =>
          enter [2, 1, i]
          change ite ..
          rw [if_pos (h i)]
        simp
      · rw [if_neg h, eq_comm, ← top_le_iff]
        rw [not_forall] at h
        obtain ⟨i, hi⟩ := h
        refine le_trans ?_ (ENNReal.summable.le_tsum' i)
        change ⊤ ≤ ite ..
        simp [hi]
    trim_le _ := (OuterMeasure.trim_eq _ .of_discrete).le
  }
  let ν : Measure α := 0
  have h : μ = ν := DiscreteMeasurableSpace.ext_of_singleton
    (fun _ => if_pos (by simp))
  have hμ : μ Set.univ = ⊤ := if_neg Set.not_countable_univ
  have hν : ν Set.univ = 0 := rfl
  apply ENNReal.top_ne_zero
  rw [← hμ, h, hν]

[Bolton Bailey]

Interesting! I am surprised to hear this is formally independent, because it seems like adding (the <1 version of) the theorem as an axiom would actually allow us to move forward with the plan for redefining PMF as a measure over the discrete measure space and unifying the API. I don't often hear of logical axioms with practical relevance like this.

[David Ledvinka]

Sorry yes I misspoke in the other thread when I said that PMF and Measure[⊤] are essentially equivalent (Aaron giving the classic counterexample). However my proposal was not to rewrite the API by replacing PMF with DiscreteMeasure but rather that one should use PMF/MFs only as a tool to define measures and then the API should be defined for measures directly so that a) any concept defined for measures is automatically defined and usable for discrete measures, b) its much easier to state any theorem at the right level of generality.

For example viewing a discrete measure (coming from a pmf) as count.withDensity p would allow one to prove theorems about both pdfs and pmfs at the same time. Viewing a discrete measure as a (possibly infinite) liner combination of diracs behaves very nicely with (simp-based) computation (as demonstrated below).

import Mathlib

open MeasureTheory Measure ENNReal

variable {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α]
-- From #33668 by Citronhat
theorem lintegral_eq_tsum (p : PMF α) (f : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂(p.toMeasure) = ∑' a, p a * f a := calc
  _ = ∫⁻ (a : α) in p.support, f a ∂p.toMeasure := by rw [p.restrict_toMeasure_support]
  _ = ∑' (a : p.support), f a * p.toMeasure {↑a} := lintegral_countable _ p.support_countable
  _ = ∑' (a : p.support), p a * f a := by
    simp_rw [p.toMeasure_apply_singleton _ (measurableSet_singleton _), mul_comm]
  _ = ∑' a, p a * f a := tsum_subtype_eq_of_support_subset (Function.support_mul_subset_left p f)

theorem pmf_eq_sum_dirac (p : PMF α) :
    p.toMeasure = sum (fun a ↦ p a • dirac a) := by
  refine ext_of_lintegral _ (fun f hf ↦ ?_)
  simp [lintegral_eq_tsum]
  --simp only [lintegral_eq_tsum, lintegral_sum_measure, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]

  theorem pmf_eq_count_with_density (p : PMF α) :
      p.toMeasure = count.withDensity p := by
    simp [count_withDensity, pmf_eq_sum_dirac]

I think its better to use these then PMF directly for the same reason I think its better to use Measure and IsProbabilityMeasure instead of ProbabilityMeasure. There is however the issue that Measure cannot be made a Monad in the sense of core Lean and there is desire for this so it may make sense to keep a PMF type or MF type for this use which can also be used as a constructor of sorts for Measures as @Peter Pfaffelhuber suggested.

[Peter Pfaffelhuber]

James E Hanson schrieb:

Specifically, you can have a $\{0,1\}$-valued measure $\mu$ on the full power set of a given set $X$ such that $\mu(X) = 1$ but $\mu(\{x\}) = 0$ for every $x \in X$.

Do you have a reference for this? The only $\{0,1\}$-valued measure I know is the dirac-measure...

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Measurable_cardinal

[James E Hanson]

Bolton Bailey said:

I don't often hear of logical axioms with practical relevance like this.

Well so first of all measurable cardinals arose from measure theory research in the 1920s and 30s. Ulam was looking at the question of what kinds of measures the full power set of a set can admit.

But they also show up in a lot of perhaps surprising places. The existence of a measurable cardinal is equivalent to any of the following:

• The existence of a set $I$ such that the natural homomorphism from $\bigoplus_I \mathbb{Z}$ to the double dual $\mathrm{Hom}(\mathrm{Hom}(\bigoplus_I \mathbb{Z},\mathbb{Z}),\mathbb{Z})$ fails to be an isomorphism.
• The existence of a discrete topological space $X$ that is not realcompact (i.e., is homeomorphic to a closed subset of a space of the form $\mathbb{R}^Y$).
• The existence of an exact functor from $\mathrm{Set}$ to $\mathrm{Set}$ that is not naturally isomorphic to the identity functor.
• The existence of a group $G$ that is not the fundamental group of any compact Hausdorff space.

The existence of a measurable cardinal also implies that for any Borel set $B \subseteq \mathbb{R}^3$, the projection of the complement of the projection of $B$ is Lebesgue measurable, which is not provable in ZFC or Lean.

[Bolton Bailey]

David Ledvinka said:

However my proposal was not to rewrite the API by replacing PMF with

Sorry, didn't mean to suggest it was your proposal, any mistaken ideas in suggestions I propose are my own.

I am nevertheless interested in a measure-theoretic redefinition of PMF because it seems like it would make it easier to align the API between PMF and the rest of measure theory. I think this could then make it easier to either get to a world where PMF is only used when necessary or at least have measure theory API more easily available to people like me who don't need to use non-pmf measures in the projects they're interested in. Does this seem reasonable?

[Bolton Bailey]

Maybe I am asking about the wrong measure space. Is there such a thing as the measure space "generated" by just sets that can be the support of PMFs (so countable sets, I guess)? Is PMF equivalent to the type of probability measures on that space?

[David Ledvinka]

Of course if you stick to countable spaces everything is fine (this is what I had in mind when I answered in the other thread) see Measure.ext_of_singleton.

In general I think that by improving the withDensity and sum/dirac APIs we can get an API that works just as well or better without the need for relying on a separate type.

[Violeta Hernández]

Bolton Bailey said:

Also, what about

theorem DiscreteMeasurableSpace.ext_of_singleton [DiscreteMeasurableSpace α] {μ ν : Measure α}
    (h : ∀ a, μ {a} = ν {a}) : μ = ν := by sorry

Does a σ-finite assumption fix this?

[Aaron Liu]

not if a measurable cardinal exists