Uniqueness in Riesz–Markov–Kakutani representation theorem

Stream: mathlib4

[Yongxi Lin (Aaron)]

Currently we don't have the uniqueness of measure in the link https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.html#RealRMK.rieszMeasure. More specifically, I want to show that if two regular measures induce the same linear functionals on the set of (compactly supported) continuous functions, then these two measures are equal. I want to formalize this part and before proceeding, I just want to confirm whether anyone is trying to formalize this theorem right now.

[Yoh Tanimoto]

@Oliver Butterley

[Oliver Butterley]

Thanks Yoh for the ping. I noticed that this was missing and three weeks ago discussed with Yoh that we should add it. I then got busy with other things and completely forgot about it.

It's an important part of the statement, it should be added. I didn't get anything done and won't have time at the moment. Great if you can add it!

[Yongxi Lin (Aaron)]

@Oliver Butterley @Yoh Tanimoto Hi Yoh and Oliver, I started formalizing today and below is my rough plan. I am using Rudin’s Real and Complex Analysis as my reference. Is it possible for you to have a look of my plan and give me some advice before I proceed? I also just want to confirm with you so that I won’t reproduce anything that is already in the Mathlib. 

import Mathlib

open MeasureTheory CompactlySupported NNReal TopologicalSpace CompactlySupportedContinuousMap

variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X]

/-Outer regular measures are determined by open sets.-/
theorem outerregular_open {μ ν : Measure X} [Measure.OuterRegular μ] [Measure.OuterRegular ν]
  (hμν : ∀ U, IsOpen U → μ U = ν U) : μ = ν := by sorry

/-Inner regular measures on open sets are determined by compact sets.-/
theorem innerregular_compact {μ ν: Measure X} (hμ : μ.InnerRegularWRT IsCompact IsOpen)
  (hν : ν.InnerRegularWRT IsCompact IsOpen) (hμν : ∀ U, IsCompact U → μ U = ν U) :
  ∀ U, IsOpen U → μ U = ν U := by sorry

/-Let μ be a measure that is finite on compact sets. Then μ induces a positive
linear functional on C_c(X, ℝ).-/
noncomputable def integralPositiveLinearMap (μ : Measure X) [OpensMeasurableSpace X]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] :
  { Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ // ∀ f : C_c(X, ℝ), 0 ≤ f → 0 ≤ Λ f} := sorry

/-Let μ be a measure that is finite on compact sets. Then μ induces a
linear functional on C_c(X, ℝ≥0).-/
noncomputable def integralLinearMap (μ : Measure X) [OpensMeasurableSpace X]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] :
  C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0 := sorry

variable [T2Space X] [LocallyCompactSpace X] [BorelSpace X]

/-Let K be a compact set contained in an open set V. Then there exists a compactly supported
continuous function f such that 0 ≤ f ≤ 1, f=1 on K and the support of f is contained in V.-/
lemma exists_compact_le_f_le_open {K V : Set X} (hK : IsCompact K)
  (hV : IsOpen V) (hKV : K ⊆ V) : ∃ (f : C_c(X, ℝ≥0)),
  Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by sorry

lemma compare_measure_of_compact_sets_ε {μ ν : Measure X} [Measure.OuterRegular ν]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (hμν : ∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), (f x : ℝ) ∂μ = ∫ (x : X), (f x : ℝ) ∂ν) :
  ∀ K, IsCompact K → ∀ (ε : NNReal), 0 < ε → ν K < ⊤ → μ K ≤ ν K + ε := sorry

lemma compare_measure_of_compact_sets {μ ν : Measure X} [Measure.OuterRegular ν]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (hμν : ∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), (f x : ℝ) ∂μ = ∫ (x : X), (f x : ℝ) ∂ν) :
  ∀ K, IsCompact K → μ K ≤ ν K := by sorry

/-If two regular measures give the same integral for every functions in C_c(X, ℝ≥0),
then they are equal.-/
theorem NNRealRMK.uniqueness1 {μ ν : Measure X} [Measure.Regular μ] [Measure.Regular ν]
  (hμν : ∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), (f x : ℝ) ∂μ = ∫ (x : X), (f x : ℝ) ∂ν) :
  μ = ν := by sorry

/-If two regular measures induce the same linear functional on C_c(X, ℝ≥0),
then they are equal.-/
theorem NNRealRMK.uniqueness2 {μ ν : Measure X} [Measure.Regular μ]
  [Measure.Regular ν] (hμν : integralLinearMap  μ = integralLinearMap  ν) :
  μ = ν := by sorry

/-NNRealRMK.rieszMeasure is a surjective function (i.e. every regular measure is induced
by a linear functional on C_c(X, ℝ≥0)).-/
theorem NNRealRMK.uniqueness3 {μ : Measure X} [Measure.Regular μ]  :
  μ = NNRealRMK.rieszMeasure (integralLinearMap μ) := by sorry

/-If two regular measures give the same integral for every functions in C_c(X, ℝ),
then they are equal.-/
theorem RealRMK.uniqueness1 {μ ν : Measure X} [Measure.Regular μ] [Measure.Regular ν]
  (hμν : ∀ (f : C_c(X, ℝ)), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν) : μ = ν := by  sorry

/-If two regular measures induce the same positive linear functional on C_c(X, ℝ),
then they are equal.-/
theorem RealRMK.uniqueness2 {μ ν : Measure X} [Measure.Regular μ]
  [Measure.Regular ν] (hμν : integralPositiveLinearMap  μ = integralPositiveLinearMap ν) :
  μ = ν := by sorry


/-RealRMK.rieszMeasure is a surjective function (i.e. every regular measure is induced
by a positive linear functional on C_c(X, ℝ)).-/
theorem RealRMK.uniqueness3 {μ : Measure X} [Measure.Regular μ]  :
  μ = RealRMK.rieszMeasure (integralPositiveLinearMap μ).2 := by sorry

[Yongxi Lin (Aaron)]

Besides I have two quick questions.

1. Do we have the following version of Urysohn's lemma in Mathlib?

variable [T2Space X] [LocallyCompactSpace X] [BorelSpace X]
/-Let K be a compact set contained in an open set V. Then there exists a compactly supported
continuous function f such that 0 ≤ f ≤ 1, f=1 on K and the support of f is contained in V.-/
lemma exists_compact_le_f_le_open {K V : Set X} (hK : IsCompact K)
  (hV : IsOpen V) (hKV : K ⊆ V) : ∃ (f : C_c(X, ℝ≥0)),
  Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by sorry

2. Somehow I cannot use NNRealRMK.integral_rieszMeasure. I have already import Mathlib, but Lean keeps telling me that unknown identifier 'NNRealRMK.integral_rieszMeasure'.

[Aaron Liu]

Can you write a #mwe?

[Aaron Liu]

There are about 10 different urysohn's lemmas in file#Topology/UrysohnsLemma but I don't see the one you want

[Yoh Tanimoto]

Yongxi Lin said:

Besides I have two quick questions.

1. Do we have the following version of Urysohn's lemma in Mathlib?

variable [T2Space X] [LocallyCompactSpace X] [BorelSpace X]
/-Let K be a compact set contained in an open set V. Then there exists a compactly supported
continuous function f such that 0 ≤ f ≤ 1, f=1 on K and the support of f is contained in V.-/
lemma exists_compact_le_f_le_open {K V : Set X} (hK : IsCompact K)
  (hV : IsOpen V) (hKV : K ⊆ V) : ∃ (f : C_c(X, ℝ≥0)),
  Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by sorry

2. Somehow I cannot use NNRealRMK.integral_rieszMeasure. I have already import Mathlib, but Lean keeps telling me that unknown identifier 'NNRealRMK.integral_rieszMeasure'.

1. not exactly the same but maybe exists_tsupport_one_of_isOpen_isClosed is enough?
2. the following works. what fails?

import Mathlib

#check NNRealRMK.integral_rieszMeasure

[Yoh Tanimoto]

Yongxi Lin said:

Is it possible for you to have a look of my plan and give me some advice before I proceed?

sure. Please add the following to the code, so that it complies immediately (such a code is called #mwe)

import Mathlib

open MeasureTheory CompactlySupported NNReal

variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X]

• I think outerregular_open is good
• maybe innerregular_compact should have also μ = ν as the conclusion
• J I should have more self-explanatory names. perhaps integralLinearMap?
• actually I thought it would be good to have a type of positive linear functionals. I guess it would be better to do so as a structure?
• shoudn't the conclusion of compare_measure_of_compact_sets be μ K ≤ ν K?
• RealRMK.uniqueness1 misses the concluslon

[Oliver Butterley]

Hi Yongxi. It's great that you are pushing ahead with this proof!

It seemed to me best to first prove:

import Mathlib
open MeasureTheory CompactlySupported
variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] [T2Space X] [BorelSpace X]

theorem eq_of_forall_integral_zero (μ : Measure X) (h : ∀ (f : X →C_c ℝ), ∫ x, f x ∂μ = 0) :
    μ = 0 := by
  refine Measure.ext (fun s hs ↦ ?_)

  sorry

And then the uniqueness would follow from the linearity of the integral. In order to prove the above I believe one could take advantage of exists_tsupport_one_of_isOpen_isClosed (as mentioned by Yoh) and show that the measure of the set is bounded by the integral which is zero. And a few more details...

@Yoh Tanimoto, what do you think? I'm often missing simple things!

[Yoh Tanimoto]

Not sure how μ = ν follows from this, as there's no linearity for measures...?

[Oliver Butterley]

:scream: I'm so sorry, I was writing something which is completely ridiculous. Thanks Yoh for pointing this out. (I have no excuse for this although it was because I was still thinking about the complex measure case.(

[Yongxi Lin (Aaron)]

I made some changes to my code and I want to address some of the questions above.

1. For the lemma innerregular_compact, I can't deduce $\mu=\nu$ without assuming $\mu$ and $\nu$ are outer regular. That is, I need outerregular_open in order to deduce innerregular_compact. I want to be general here so I did not put $\mu=\nu$ as the conclusion of innerregular_compact.
2. We do have PositiveLinearMap in Mathlib.
3. exists_tsupport_one_of_isOpen_isClosed is not really the version of Urysohn's lemma I want because in this version, one needs the open set to have compact closure. The version of Urysohn's lemma that I want should follow easily from exists_continuous_one_zero_of_isCompact.

[Oliver Butterley]

Ah, PositiveLinearMap was added to Mathlib at the end of March this year and so wasn't yet available when RealRMK was written. :rofl:

[Yoh Tanimoto]

1. so maybe the comment should say "Inner regular measures on open sets are determined by compact sets"?
2. right, please use this definition
3. right, but you are assuming LocallyCompactSpace X, so you can take an open subset whose closure is compact. Beware that exists_continuous_one_zero_of_isCompact assumes RegularSpace X

[Yongxi Lin (Aaron)]

Oh right this is my fault, my comment is not correct. I'll change it.

[Yongxi Lin (Aaron)]

Isn't a locally compact T2 space regular? I didn't really remember all my point-set topology so I may not be correct.

[Aaron Liu]

import Mathlib

variable {X : Type*} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X]

-- succeeds
#synth RegularSpace X

[Yoh Tanimoto]

well ok, I think for the case in hand either way is fine

[Yongxi Lin (Aaron)]

I am almost done in substituting sorrys with actual proofs in my outline. Before I make a pull request, I just want to know how I should include PositiveLinearMap in my code. Should I just replace the sutype { Λ : C_c(X, ℝ) →ₗ[ℝ] ℝ // ∀ f : C_c(X, ℝ), 0 ≤ f → 0 ≤ Λ f} with PositiveLinearMap ℝ C_c(X, ℝ) ℝ? It seems like that I should also change the existing code in https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.html#RealRMK.rieszMeasure.

[Yoh Tanimoto]

I would be glad if you could change the existing code. Probabily it's a good idea to make a separate PR to switch to PositiveLinearMap

[Yongxi Lin (Aaron)]

OK I'll make two PRs then.

[Yoh Tanimoto]

apparently IsOrderedAddMonoid C(X, α) is missing even if X α has appropriate instances. Should this be added?

import Mathlib

variable (X α  : Type*) [TopologicalSpace X] [TopologicalSpace α] [AddCommMonoid α] [ContinuousAdd α] [PartialOrder α]
[IsOrderedAddMonoid α]

#synth IsOrderedAddMonoid (X → α)
#synth PartialOrder C(X, α)
#synth AddCommMonoid C(X, α)
-- #synth IsOrderedAddMonoid C(X, α) fails

instance : IsOrderedAddMonoid C(X, α) where
  add_le_add_left _ _ hfg c := add_le_add_left hfg c

[Yoh Tanimoto]

#27994

[Jireh Loreaux]

I would swear I've written this instance already. :thinking:

[Yoh Tanimoto]

some natural stuff is missing! There isn't PartialOrder C₀(X, α) either.

import Mathlib

open ZeroAtInfty CompactlySupported

variable (α β : Type*) [TopologicalSpace α] [TopologicalSpace β] [AddCommMonoid β] [ContinuousAdd β] [PartialOrder β] [IsOrderedAddMonoid β]
-- fails #synth PartialOrder C₀(α, β)
-- fails #synth IsOrderedAddMonoid C₀(α, β)
#synth PartialOrder C_c(α, β)

[Yoh Tanimoto]

ah probably you wrote this? BoundedContinuousFunction.instIsOrderedAddMonoid

[Thomas Zhu]

#28059 changes RMK to use PositiveLinearMap

[Yoh Tanimoto]

thanks!

[Yongxi Lin (Aaron)]

I formazlied uniqueness in RMK in this PR #28061, which depends on #28059