Riesz representation theorem

Stream: maths

[Yury G. Kudryashov]

Hi, it looks like the formalization of https://en.wikipedia.org/wiki/Riesz%E2%80%93Markov%E2%80%93Kakutani_representation_theorem started in !3#16367 was never completed.

[Yury G. Kudryashov]

Where can I find the informal proof that was being formalized in this PR?

[Johan Commelin]

I don't know the author of that PR? There are two J. Reimann's on zulip though...

[Andrew Yang]

According to the discussion here The author is probably @Jesse Reimann

[Jireh Loreaux]

I think @Yoh Tanimoto might have been working on this as well.

[Jesse Reimann]

Yes that was me! The proof was done in Lean 3, I think @Kalle Kytölä has previously mentioned something about porting it to Lean 4, but I don't know what the status of that is :smile:

[Kalle Kytölä]

@Jesse Reimann proved Riesz-Markov-Kakutani representation theorem for compact Hausdorff spaces (which have some nice aspects for probability applications and which can be used to get the locally compact case, too, but this generalization was not done) in Lean3. The Mathlib PRs of that work got stalled for a long time because there were no multiplication and (truncated) subtraction operations defined on bounded continuous nonnegative functions, which were used in the proof.

Since then, my understanding is that @Yoh Tanimoto proved Riesz-Markov-Kakutani representation theorem in Lean4 for locally compact Hausdorff spaces (i.e. directly the natural generality), and it was discussed in #12290 that although the multiplication and subtraction sticking points were finally fixed in #12790 and #12559, Yoh's version seemed the right way forward.

(If that assessment has changed, it is possible to port Jesse's code to Lean4 and refactor it to use the subtraction and multiplication instead of the workarounds that were needed originally. But the porting of Jesse's code to Lean4 is not done yet.)

[Jireh Loreaux]

It looks like #12290 is currently stuck on #12266 which is marked help-wanted. I think @Yury G. Kudryashov promised to have a look, but that hasn't yet happened.

[Kalle Kytölä]

Yury G. Kudryashov said:

Where can I find the informal proof that was being formalized in this PR?

The informal proof that Jesse originally started with was Rudin's proof in Real and Complex Analysis, Chapter 2 (except we did simplifications for compact rather than locally compact case with my probability applications in mind). But at some point we noticed that Mathlib had good existing results on docs#MeasureTheory.Content, and we switched to a version that does not literally follow any reference I know of. Sorry about an unhelpful answer! But basically the version Jesse formalized is Rudin, rewritten using existing results on contents, and simplified for the compact case (first).

[Yoh Tanimoto]

Yes, if we want to prove the RMK theorem on a locally compact T2 space, I think we need something like #12266 or its variation as partition of unity to prove that the measure constructed with rieszContentAux gives back the functional Λ.

There is another question/option of the field, either Real or NNReal. My understanding is that we should first prove it for NNReal but I wrote #12290 for Real. To switch to NNReal, Kalle's PRs should suffice, but I haven't worked on it. Probably one can prove that rieszContentAux is indeed a content without #12266.

[Kalle Kytölä]

Correct, showing that rieszContentAux is indeed a docs#MeasureTheory.Content, became short after the subtraction and multiplication of bounded continuous functions were generalized (included below again). The remaining parts after that of the compact Hausdorff case were to (1) obtain a measure from the content and (2) characterize it as the unique measure whose docs#MeasureTheory.lintegral reproduces the given positive linear functional. Those are a bit longer than the code below, but not huge. However, this approach would indeed leave one to handle the locally compact case separately, so Yoh's handling of that directly sounded appealing.

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 Λ

[Kalle Kytölä]

And yes, there was the question of how much to use NNReal and at which point to get the results to Real. I am almost sure we want both kinds of versions in Mathlib, and which one to use first, and which one to obtain as a consequence, I view it as a bit of an implementation detail choice that different authors would have different preferences about. (I remember @Anatole Dedecker was not enthusiastic about working with NNReal-linear and NNReal-valued functionals on continuous NNReal-valued functions as a way to guarantee the positivity of the functional, but to me this made sense, because measures are fundamentally already ENNReal valued ENNReal-linear functionals on ENNReal-valued functions, via the Lebesgue integral. Talking about positivity of the functional and jumping directly to Bochner integral I did not find as appropriate, because Bochner integral is meant for more general value spaces than the one-dimensional linearly ordered one where we have the notion of positivity. Anyway, once either implementation is done, getting the other is easy.)

[Jireh Loreaux]

I've thought a bit about how to deal with selfadjoint and positive linear functionals but I don't have any time to write much about it today. I'll try to remember to post my thoughts here soon. However, I would agree with Anatole that you probably want to stick with ℝ, and avoid ℝ≥0. That being said, in the continuous functional calculus, we have opted for an ℝ≥0 version too, and I think it is the right decision, despite the major headaches it causes sometimes. I think that the situation of positive linear functionals is a bit different though.

[Yury G. Kudryashov]

I'm sorry for stalling this in review. I'll do my best to review it tonight.

[Yoh Tanimoto]

as for #12266, probably I should write a variation of exists_isSubordinate_of_prop where X is locally compact and T2 but s is compact?

[Yury G. Kudryashov]

I'm sorry for another delay. I'm too busy at my day job. I'll have a look in ~3h after a meeting at the office.

[Yury G. Kudryashov]

Is there a new Urysohn's-like statement (for s and t with some properties, there exist a continuous function that is 0 on s and 1 on t) behind the new "partition of unity" statement? If yes, could you please formulate it (formally or informally)?

[Yoh Tanimoto]

I think I need PartitionOfUnity.exists_isSubordinate with T2Space X but IsCompact s. The current theorem takes NormalSpace X because so does BumpCovering.exists_isSubordinate, which depends on the shrinking lemma. But I guess I can prove an analogue if X is T2 locally compact and s is compact?

[Yury G. Kudryashov]

Could you please revert to a version that had all the theorems you want with complete proofs?

[Yury G. Kudryashov]

I'll look into a way to make it work with our API then.

[Yoh Tanimoto]

I restored the old version in Topology.UrysohnLemma. Meanwhile I'm trying to see if the shrinking lemma can be adapted to my case.

[Yury G. Kudryashov]

I'll have a look tonight.

[Yury G. Kudryashov]

The PR description talks about normal T2 spaces while your replies indicate that your goal is to drop the NormalSpace assumption.

[Yury G. Kudryashov]

It looks like the theorem doesn't assume [NormalSpace].

[Yoh Tanimoto]

sorry, indeed "normal T2 space" didn't make sense. I meant "locally compact T2 space" (updated).

This PR splitted from #12290, where the proof that the measure gives back Λ is missing, but is done in https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/RMK/linearRMK.lean . Here I need #12266. First @Jireh Loreaux pointed out that I could weaken NormalSpace to T2Space, then you and @Floris van Doorn suggested to use PartitionOfUnity instead of Urysohn's lemma.

[Yury G. Kudryashov]

About the suggestion to use PartitionOfUnity: you can prove existence of a docs#BumpCovering using your approach, then get a docs#PartitionOfUnity for free.

[Yury G. Kudryashov]

This way you don't need to redo the algebraic part of the proof.

[Yoh Tanimoto]

I see, by "your approach" do you mean changing NormalSpace to LocallyCompactSpace T2Space with IsCompact s in the Shrinking lemma ?

[Yury G. Kudryashov]

Also, I think about introducing an intermediate predicate IsUrysohnsPair (s t : Set X) that says ∃ f : X → Real, Continuous f ∧ EqOn f 0 s ∧ EqOn f 1 t and deduce various corollaries from there.

[Yury G. Kudryashov]

By "your approach" I mean "whatever you do in your long proof of your main theorem, I haven't read the proof yet".

[Yury G. Kudryashov]

BTW, it should be possible to generalize from T2Space to R1Space. Also note that [R1Space X] [LocallyCompactSpace X] implies RegularSpace X, so you can reuse some of @Sébastien Gouëzel 's work on Urysohn's lemma for locally compact regular spaces.

[Yury G. Kudryashov]

It looks like your Urysohn's-like lemma doesn't need X to be a locally compact space, so probably you can prove it before Sébastien's and use it to deduce Sébastien's version in case of a locally compact space.

[Yoh Tanimoto]

well, currently BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop depends on NormalSpace, so I thought we needed a variation for T2Space (or R1Space) (+ LocallyCompactSpace), isn't it correct?

[Yury G. Kudryashov]

Note: please don't start the IsUrysohnsPair refactor, I want to do it myself.

[Yury G. Kudryashov]

I think that a part of your proof constructs a BumpCovering (without using its definition).

[Yury G. Kudryashov]

I haven't read your proof in an editor, so I don't understand the details yet. I can do it tomorrow.

[Yoh Tanimoto]

probably g in my proof is a BumpCovering, I will have to check. But at this point isn't it better to have a variation of the shrinking lemma? On the other hand, it's not clear to me how to drop LocallyCompactSpace.

[Yury G. Kudryashov]

"Add a version of the shrinking lemma" is a possible way to go.

[Yury G. Kudryashov]

But I need to better understand your proof before giving this advice.

[Yoh Tanimoto]

I see

[Yoh Tanimoto]

@Jesse Reimann do you have the Lean 3 code for the characterization of the Riesz measure (that the original linear functional Λ is written as the integral over the measure)? Is your Λ NNReal-linear? If so, how did you show the equality, did you use le_antisymm and proved the both inequalities?

[Bas Spitters]

Aside, it's possible to factor this theorem via locales and valuations. In that way, one could fx generalize the proof to condensed type theory, or other constructive type theories.
http://www.doi.org/10.1007/s11083-010-9147-3
http://arxiv.org/abs/0808.2705

[Kalle Kytölä]

Yoh Tanimoto said:

Jesse Reimann do you have the Lean 3 code for the characterization of the Riesz measure (that the original linear functional Λ is written as the integral over the measure)? Is your Λ NNReal-linear? If so, how did you show the equality, did you use le_antisymm and proved the both inequalities?

I have some version of Jesse's old code. I am not sure what I have is the most up to date version, and I also no longer have Lean3 to even check that it compiles, and in any case the code required ad hoc workarounds that have become unnecessary now that subtraction and multiplication on BoundedContinuousFunction just work even for functions with NNReal values.

The key is certainly to prove one direction of the inequality directly, and Jesse proved:

lemma functional_le_riesz_integral (f : X →ᵇ ℝ≥0) :
    Λ f ≤ (∫⁻ x, ( coe ∘ f ) x ∂(riesz_meas Λ )).to_nnreal :=

I'm not sure how much the proof was ever cleaned up, this is certainly one of the longer proofs. (The strategy was basically the same as in Rudin's book, except that the compact case allowed for some simplifications, if I remember correctly.)

This result is also enough. If we were working with real values, then the standard trick (after le_antisymm) to get the other inequality would be to apply to $f$ and $-f$, and use $\R$-linearity. But also with NNReal values, a similar trick still works. Namely, one can apply this to both $f$ and $g := M - f$ where M := nndist f 0 is "$M := \|f\|_\infty$". (In Jesse's code, this part used our ad hoc bounded_continuous_function.nnreal_sub (bounded_continuous_function.const X M) f, and became unnecessarily messy, but with current Mathlib it can be done in a clean way just using the now generalized subtraction on bounded continuous functions).

I hope this at least clarifies the route that Jesse took in her proof. It is just like @Yoh Tanimoto suggests, plus the observation that one direction of the inequality is enough, even with NNReal values.

[Yoh Tanimoto]

@Kalle Kytölä thanks for your reply! I suspected this, and it's a problem for my current attempt, because M - f is surely bounded, but not compactly supported...

[Kalle Kytölä]

Ouch, I see. That looks more annoying to deal with.

I guess in principle one could replace $M$ with some compactly supported function that is larger than $f$. But I don't know how much of a headache that is to deal with, since its integral is not just an obvious value.

[Yoh Tanimoto]

I'm not sure, if you take a function g larger than f, I guess you need the equality of Λ and the integral for g, or do you have something else in mind?

[Kalle Kytölä]

I'm sorry, yes, you are right. This just looks harder to deal with.