feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

[yoh-tanimoto]

define rieszContentAux under Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f) and prove that it is a Content.

Motivation : This will be a basis for example, of the spectral decomposition of self-adjoint operators on Hilbert spaces.

Depends on #12266 for a variation of Urysohn's lemma. Perhaps some refactoring is still needed. More importantly, we should still introduce C_c

Proving (∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), f x ∂(MeasureTheory.Content.measure (rieszContent Λ hΛ)) = Λ f) is available here https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean not yet included in this PR.

[sgouezel]

Instead of creating a new file, can you put your additions in the already existing file on the Riesz content? Otherwise, this makes the PR very hard to review (I don't know what is new material and what was already there).

[yoh-tanimoto]

OK sorry, I wasn't sure whether I should change the existing file because I changed the whole setting from ℝ≥0 to ℝ. Now I removed the new file and replaced the old file with mine.

[sgouezel]

Oops, my bad, I hadn't noticed that you had switched from NNReal to Real. Can you explain the reason for this choice? It seems to me that most things down the road should be easier using NNReal-valued functions (in particular because the topology on spaces of measures is defined using such functions), so I'd rather use them unless they create a difficulty somewhere.

[yoh-tanimoto]

I changed from NNReal to Real because I have in mind the application of the RMK theorem to prove the spectral decomposition. There one would need even complex valued functionals, complex-valued measures, and so on, but I thought it was a good start to use linear structures rather than NNReal. What do you think?

[sgouezel]

For complex measures, one should definitely use complex-valued functions. For real measures, real-valued functions. And for measures in the usual sense, which are nonnegative, then NNReal-valued functions looks like the most natural choice. We have already code duplication between measures and vector-valued measures, but this seems unavoidable.

[yoh-tanimoto]

so do you mean that I should make a new file, say "RealRieszMarkovKakutani.lean" and keep the NNReal version as is?

[sgouezel]

I mean for now we should just use NNReal and do everything with them. Once we have Riesz-Markov-Kakutani for measures, we may start thinking on what we want to do with real measures or complex measures (or vector-valued measures), but it wouldn't make sense to do it before we complete it for usual measures, because when doing it we will learn a lot.

[yoh-tanimoto]

Ok, then I will bring back NNReal and the Real version as a separate file

[sgouezel]

Ok, then I will bring back NNReal and the Real version as a separate file

For now, I'd say we shouldn't even have the Real version at all, and only do the NNReal one.

[yoh-tanimoto]

I see, I will do that.

[yoh-tanimoto]

I tried to do the NNReal version myself, and I found that the proof of additivity rieszContentAux_eq_add is painful: one should take, using Urysohn's lemma, a function g which is 0 on K₁ and 1 on K₂, but then

• one has to prove that g : X →ᵇ ℝ≥0
• one has to prove that 1 - g : X →ᵇ ℝ≥0
• Mul is not given for X →ᵇ ℝ≥0, so one has to prove that f * (1-g) : X →ᵇ ℝ≥0

I think this is what Kalle described on Zulip.

It seems that he and Jesse have the plan to do it, so I would leave this to them.

On the other hand, the Real version is done up to a variation of Urysohn's lemma. Let me know what I should do with this PR.

[kkytola]

I tried to do the NNReal version myself, and I found that the proof of additivity rieszContentAux_eq_add is painful: one should take, using Urysohn's lemma, a function g which is 0 on K₁ and 1 on K₂, but then

* one has to prove that `g : X →ᵇ ℝ≥0`
* one has to prove that `1 - g : X →ᵇ ℝ≥0`
* `Mul` is not given for `X →ᵇ ℝ≥0`, so one has to prove that `f * (1-g) : X →ᵇ ℝ≥0`

I think this is what Kalle described on Zulip.

This is indeed exactly the issue why our PRs stalled, and as I tried to quickly comment on in Zulip, explaning that we had discussed the necessary fixes for that with @ADedecker (before some related things were changed, rendering some of the earlier conclusions potentially outdated).

I think it is important to improve Mathlib so that BoundedContinuousFunction with values in ℝ≥0 work reasonably (e.g. they have a multiplication and truncated subtraction). I think this fix should be done regardless of the exact implementation path we choose towards Riesz-Markov-Kakutani, and I will try to get started with that fix in the near future.

In an ideal mathlib-world, measures and "Lebesgue integration theory" (lintegral, i.e. integration of nonnegative functions) should play well with nonnegative bounded continuous functions. But I agree that in the current state of things, working with NNReal is making some things unnecessarily painful. Therefore I don't currently have a clear opinion on what is the most reasonable course of action for getting some implementation of Riesz-Markov-Kakutani to Mathlib.

[yoh-tanimoto]

thanks for your comments. I think I understand the need to add more material about BoundedContinuousFunction as you say.

As for this PR, I defined rieszContentNonneg, which takes RestrictNonneg Λ hΛ : C(X, ℝ≥0) → ℝ≥0, so this essentially eqivalent to rieszContentAux in the file RieszMarkovKakutani. (I need to change C(X, ℝ≥0) to C_c(X, ℝ≥0), but waiting for the merge of #12402). I prove the additivity of it showing the additivity of the linear version of rieszContentAux and showing that they take the same values.

[kkytola]

I made #12559 which enables subtraction for nonnegative bounded continuous functions. If the model (new type class and otherwise minimal changes) is considered reasonable, I will do a similar PR to allow also multiplication of nonnegative bounded continuous functions.

[kkytola]

Now that #12790 and #12559 are in Mathlib and one can subtract and multiply bounded continuous functions, showing that the rieszContentAux gives rise to an actual content (rieszContent below) is simple. The following are translated steps from Jesse's Lean3 proof of this part, whose PRs unfortunately stalled exactly because subtraction and multiplication of bounded continuous functions needed to be done properly in Mathlib. (Jesse continued from here to construct the measure and characterize it.)

import Mathlib

open scoped Classical NNReal ENNReal BoundedContinuousFunction
open MeasureTheory Set Function

variable {Z : Type} [TopologicalSpace Z] [NormalSpace Z]

lemma exists_bounded_zero_one_of_closed_nnreal 
    {s t : Set Z} (s_closed : IsClosed s) (t_closed : IsClosed t) (disj : Disjoint s t) :
    ∃ (f : Z →ᵇ ℝ≥0), EqOn f 0 s ∧ EqOn f 1 t ∧ ⇑f ≤ 1 := by
  obtain ⟨g, g_zero_on_s, g_one_on_t, g_bdd⟩ := exists_bounded_zero_one_of_closed s_closed t_closed disj
  refine ⟨g.nnrealPart, ?_, ?_, ?_⟩
  · intro x x_in_s; simp [g_zero_on_s x_in_s]
  · intro x x_in_t; simp [g_one_on_t x_in_t]
  · intro x; simp [(g_bdd x).2]

lemma exists_sum_one_of_closed_nnreal 
    {s t : Set Z} (s_closed : IsClosed s) (t_closed : IsClosed t) (disj : Disjoint s t) :
    ∃ (f₁ f₂ : Z →ᵇ ℝ≥0), EqOn f₁ 1 s ∧ EqOn f₂ 1 t ∧ f₁ + f₂ = 1 := by
  obtain ⟨f, f_zero_on_s, f_one_on_t, f_bdd⟩ := exists_bounded_zero_one_of_closed_nnreal s_closed t_closed disj
  refine ⟨1 - f, f, ?_, ?_, ?_⟩
  · intro x x_in_s; simp [f_zero_on_s x_in_s]
  · intro x x_in_t; simp [f_one_on_t x_in_t]
  · ext x
    simp only [BoundedContinuousFunction.coe_add, BoundedContinuousFunction.coe_sub,
               BoundedContinuousFunction.coe_one, Pi.add_apply, Pi.sub_apply, Pi.one_apply, NNReal.coe_add,
               NNReal.coe_one]
    norm_cast
    exact tsub_add_cancel_of_le (f_bdd x)

variable {X : Type} [TopologicalSpace X] [CompactSpace X] [T2Space X]
variable [MeasurableSpace X] [BorelSpace X]
variable (Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0)

lemma rieszContentAux_union {K₁ K₂ : TopologicalSpace.Compacts X} (disj : Disjoint (K₁ : Set X) K₂) :
    rieszContentAux Λ (K₁ ⊔ K₂) = rieszContentAux Λ K₁ + rieszContentAux Λ K₂ := by
  refine le_antisymm (rieszContentAux_sup_le Λ K₁ K₂) ?_
  refine le_csInf (rieszContentAux_image_nonempty Λ (K₁ ⊔ K₂)) ?_
  intro b ⟨f, ⟨hf, Λf_eq_b⟩⟩
  obtain ⟨g₁, g₂, hg₁, hg₂, sum_g⟩ := exists_sum_one_of_closed_nnreal K₁.isCompact.isClosed K₂.isCompact.isClosed disj
  have f_eq_sum : f = g₁ * f + g₂ * f := by simp [← RightDistribClass.right_distrib, sum_g]
  rw [← Λf_eq_b, f_eq_sum, map_add]
  have aux₁ : ∀ x ∈ K₁, 1 ≤ (g₁ * f) x := by
    intro x x_in_K₁
    simp [hg₁ x_in_K₁, hf x (mem_union_left _ x_in_K₁)]
  have aux₂ : ∀ x ∈ K₂, 1 ≤ (g₂ * f) x := by
    intro x x_in_K₂
    simp [hg₂ x_in_K₂, hf x (mem_union_right _ x_in_K₂)]
  exact add_le_add (rieszContentAux_le Λ aux₁) (rieszContentAux_le Λ aux₂)

noncomputable def rieszContent (Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) : Content X where
  toFun := rieszContentAux Λ
  mono' := fun _ _ ↦ rieszContentAux_mono Λ
  sup_disjoint' := fun _ _ disj _ _ ↦ rieszContentAux_union Λ disj
  sup_le' := rieszContentAux_sup_le Λ

[yoh-tanimoto]

Nice! I am not sure how to proceed: I wrote myself the characterization of the measure for linear Λ, although it needs much refactoring (one remaining sorry is just a variation of Urysohn's lemma, I am planning to add it in a separate PR). https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean

The bundled definition of compactly supported functions is underway #12402

[kkytola]

Nice! I am not sure how to proceed: I wrote myself the characterization of the measure for linear Λ, although it needs much refactoring (one remaining sorry is just a variation of Urysohn's lemma, I am planning to add it in a separate PR). https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean

The bundled definition of compactly supported functions is underway #12402

Yes, I'm not sure what is the best way forward either!

For probability theory purposes, since convergence in distribution was defined with bounded continuous NNReal-valued functions, I would anyway like to have the bounded continuous function version of Riesz representation theorem on compact Hausdorff spaces. This was a part of my planned Prokhorov's theorem proof, which I haven't done yet, however. Of course for locally compact spaces one needs your compactly supported continuous functions anyway! So both choices come with a trade-off.

To clarify a bit, I thought on compact spaces it was worth having the bounded continuous function version, since the dual norm topology then coincides with the total variation distance on finite measures and probability measures (because bounded continuous functions readily have the sup-norm instance), whereas the weak-* topology is exactly the topology of convergence in distribution. (Ok, to get the literal dual norm, one would have to cast to real values, but the weak-* topology would work directly on the NNReal semiring module BoundedContinuousFunction X NNReal.)

So I still don't have a clear view on what is the best way to implement Riesz representation theorem in Mathlib (but I would definitely like to have it in Mathlib!), although I admit to being somewhat attached to the idea that it would work seamlessly with probability theory and this is what guided my suggestion for Jesse's implementation. However, if Riesz representation is implemented with compactly supported bounded functions, then I would just add some glue to connect it to probability theory. And maybe the locally compact case is then more straightforward (Jesse and I did not do that).

Sorry that this is not really a review of your PR, but rather a continuation from the discussion on Zulip.

Mainly, I think much of this PR can be simplified, and I wanted to at least mention that now NNReal values are no longer the big problem that they were up until now. (They are still occasionally harder to work with than real values, but on the other hand, they are somewhat more consistent with the measure theory part of the library).

[kkytola]

Nice! I am not sure how to proceed: I wrote myself the characterization of the measure for linear Λ, although it needs much refactoring (one remaining sorry is just a variation of Urysohn's lemma, I am planning to add it in a separate PR). https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean

The bundled definition of compactly supported functions is underway #12402

Actually, since you have the RMK theorem for the general locally compact case, I now think the best approach for Mathlib is indeed to get your version to Mathlib. (Jesse and I never wrote more than the compact case.) For certain probability purposes I will still want the bounded continuous function spelling, but it should be easy (and natural for Mathlib) to derive it from general case that you have. I will try to help review your PRs about that, but I'm not very experienced with reviewing and it might still take at least a week before I get to properly trying. Overall, it is great that you have the general RMK and that you are PRing it. Thank you!

[yoh-tanimoto]

thank you very much for your comments!

I think, as you say, specializing the locally compact case to the compact case is easy, indeed there are liftCompactlySupported and compactlySupportedContinuousMapClass.ofCompact. (they are not instances to avoid loop? I just followed what is done for ZeroAtInfty)

There is another question between Real/NNReal. @sgouezel suggested that such a code duplication is unavoidable. So maybe this PR should be done in NNReal and I will make a separate PR with Real?

[YaelDillies]

I've taken the freedom to mark this PR as depending #12266 since this is what you wrote yourself but without the - [ ] depends on: syntax

[github-actions[bot]]

PR summary 0b28cc9c37

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Order.Interval.Set.Union (new file)	424
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (new file)	2101

---

Declarations diff

+ CompactlySupportedContinuousMap.monotone_of_nonneg + Ico_subset_biUnion_Ico + Ioc_subset_biUnion_Ioc + exists_open_approx + integral_rieszMeasure + le_rieszMeasure_tsupport_subset + range_cut_partition + rieszMeasure + rieszMeasure_le_of_eq_one

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[yoh-tanimoto]

The part of rieszContentRegular is already split #20040. Probably I can split the contents of different files separately, if that is more appropriate.

[YaelDillies]

Ah great, I was mistaken by the lack of - [ ] depends on:

[yoh-tanimoto]

probably I should define a bundled class of positive linear functionals?

[YaelDillies]

Whoops sorry, I commented on the wrong PR again 🙈 Would you mind applying the comments in the right places?

[yoh-tanimoto]

I implemented changes to RieszMarkovKakutani.lean first in #20040 then merged them to this PR.

[sgouezel]

Do you think it would be possible to cut the main proof into several sublemmas that would highlight the different steps in the proof? In general, it's easier to read and to maintain this way.

Also, could you update the PR description to match the current content?

[YaelDillies]

I'm personally a bit confused about where each part of the proof goes. I would have expected the real and nnreal versions of rieszMeasure to be in the same file. Any reason they're not?

[yoh-tanimoto]

I will try splitting the proof into some parts, maybe those getting E, V. But I'm not sure how to split the part doing actual estimates. Do you have any suggestion?

RealRMK.rieszMeasure can be in the file RieszMarkovKakutani, no particular reason why it is in RealRMK. yet the proof of the RMK theorem must be in different files in the current implementation, because first I prove the Real-version, then I need to import it for the NNReal-version, say NNRealRMK. Should I maybe make a folder RieszMarkovKakutani, and the current file will be Basic?

[YaelDillies]

Yes, a folder would make sense!