First

Author: CoolRmal

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/NNReal.lean

@@ -55,4 +55,61 @@ theorem lintegral_rieszMeasure (f : C_c(X, ℝ≥0)) : ∫⁻ (x : X), f x ∂(r
   exact Continuous.integrable_of_hasCompactSupport (by fun_prop)
     (HasCompactSupport.comp_left f.hasCompactSupport rfl)
 
+/-If two regular measures give the same integral for every function in `C_c(X, ℝ≥0)`, then they
+are equal.-/
+theorem eq_of_integral_eq_on_Cc {μ ν : Measure X} [Measure.Regular μ] [Measure.Regular ν]
+    (hμν : ∀ (f : C_c(X, ℝ≥0)), ∫ (x : X), (f x : ℝ) ∂μ = ∫ (x : X), (f x : ℝ) ∂ν) : μ = ν := by
+  apply RealRMK.eq_of_integral_eq_on_Cc
+  intro f
+  calc
+    ∫ (x : X), f x ∂μ
+      = ∫ (x : X), ↑(f x).toNNReal ∂μ - ∫ (x : X), ↑(-f x).toNNReal ∂μ := by
+      apply integral_eq_integral_pos_part_sub_integral_neg_part
+      exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2
+    _ = ∫ (x : X), ↑(f x).toNNReal ∂ν - ∫ (x : X), ↑(-f x).toNNReal ∂ν:= by
+      have h1 : ∫ (x : X), ((f x).toNNReal : ℝ) ∂μ = ∫ (x : X), ((f x).toNNReal : ℝ) ∂ν := by
+        refine hμν ⟨⟨Real.toNNReal ∘ f, ?_⟩, ?_⟩
+        · exact continuous_real_toNNReal.comp f.1.2
+        · exact HasCompactSupport.comp_left (g := Real.toNNReal) f.2 Real.toNNReal_zero
+      have h2 : ∫ (x : X), ((-f x).toNNReal : ℝ) ∂μ = ∫ (x : X), ((-f x).toNNReal : ℝ) ∂ν := by
+        refine hμν ⟨⟨Real.toNNReal ∘ (-f), ?_⟩, ?_⟩
+        · exact continuous_real_toNNReal.comp (-f).1.2
+        · exact HasCompactSupport.comp_left (g := Real.toNNReal) (-f).2 Real.toNNReal_zero
+      rw [h1, h2]
+    _ = ∫ (x : X), f x ∂ν := by
+      symm
+      apply integral_eq_integral_pos_part_sub_integral_neg_part
+      exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2
+
+/-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 :=
+  CompactlySupportedContinuousMap.toNNRealLinear (RealRMK.integralPositiveLinearMap μ)
+
+/-If two regular measures induce the same linear functional on `C_c(X, ℝ≥0)`, then they are equal.-/
+theorem eq_of_eq_integralLinearMap {μ ν : Measure X} [Measure.Regular μ]
+    [Measure.Regular ν] (hμν : integralLinearMap μ = integralLinearMap ν) : μ = ν := by
+  apply eq_of_integral_eq_on_Cc
+  intro f
+  simp only [integralLinearMap, RealRMK.integralPositiveLinearMap, PositiveLinearMap.mk₀,
+    toNNRealLinear_inj, PositiveLinearMap.mk.injEq, LinearMap.mk.injEq, AddHom.mk.injEq] at hμν
+  simpa using congr_fun hμν (CompactlySupportedContinuousMap.toReal f)
+
+/-The Riesz measure induced by a linear functional on `C_c(X, ℝ≥0)` is regular.-/
+instance rieszMeasure_regular (Λ : C_c(X, ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) : (rieszMeasure Λ).Regular :=
+  Content.regular (rieszContent Λ)
+
+/-- NNRealRMK.rieszMeasure is a surjective function. That is, every regular measure is induced by a
+positive linear functional on `C_c(X, ℝ≥0)`. -/
+theorem rieszMeasure_surjective {μ : Measure X} [Measure.Regular μ] :
+    μ = rieszMeasure (integralLinearMap μ) := by
+  apply eq_of_integral_eq_on_Cc
+  intro f
+  trans ((integralLinearMap μ) f : ℝ)
+  · simp [← toReal_apply]
+    rfl
+  · exact (integral_rieszMeasure (integralLinearMap μ) f).symm
+
 end NNRealRMK

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

@@ -3,10 +3,9 @@ Copyright (c) 2024 Yoh Tanimoto. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yoh Tanimoto, Oliver Butterley
 -/
+import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
-import Mathlib.MeasureTheory.Integral.Bochner.Set
 import Mathlib.Order.Interval.Set.Union
-import Mathlib.Algebra.Order.Module.PositiveLinearMap
 
 /-!
 # Riesz–Markov–Kakutani representation theorem for real-linear functionals
@@ -23,6 +22,8 @@ continuous functions have compact support.
 * `RealRMK.rieszMeasure`: the measure induced by a real linear positive functional.
 * `RealRMK.integral_rieszMeasure`: the Riesz–Markov–Kakutani representation theorem for a real
   linear positive functional.
+* `RealRMK.eq_of_integral_eq_on_Cc`: the uniqueness of the representing measure in the
+  Riesz–Markov–Kakutani representation theorem.
 
 ## Implementation notes
 
@@ -339,4 +340,127 @@ theorem integral_rieszMeasure (f : C_c(X, ℝ)) : ∫ x, f x ∂(rieszMeasure Λ
   -- prove the inequality for `f`
   · exact integral_riesz_aux Λ f
 
+lemma compare_measure_of_compact_sets {μ ν : Measure X} [Measure.OuterRegular ν]
+    [MeasureTheory.IsFiniteMeasureOnCompacts ν] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
+    (hμν : ∀ (f : C_c(X, ℝ)), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν) :
+  ∀ K, IsCompact K → μ K ≤ ν K := by
+  intro K hK
+  apply ENNReal.le_of_forall_pos_le_add
+  intro ε hε hν
+  have lem1 : μ K ≠ ⊤ := by
+    rw [← lt_top_iff_ne_top]
+    exact MeasureTheory.IsFiniteMeasureOnCompacts.lt_top_of_isCompact hK
+  have lem2 : ν K ≠ ⊤ := by rw [← lt_top_iff_ne_top]; exact hν
+  rw [← ENNReal.coe_toNNReal lem1, ← ENNReal.coe_toNNReal lem2,
+    ← ENNReal.coe_add, ENNReal.coe_le_coe, ← NNReal.coe_le_coe,
+    NNReal.coe_add, ← ENNReal.toReal, ← ENNReal.toReal]
+  have hV : ∃ V ⊇ K, IsOpen V ∧ ν V ≤ ν K + ε := by
+    exact Set.exists_isOpen_le_add K ν (ne_of_gt (ENNReal.coe_lt_coe.mpr hε))
+  rcases hV with ⟨V, pV1, pV2, pV3⟩
+  have VltTop : ν V < ⊤ := by
+    apply lt_of_le_of_lt
+    · exact pV3
+    · rw [WithTop.add_lt_top]; constructor
+      · exact hν
+      · exact ENNReal.coe_lt_top
+  have hf : ∃ (f : C_c(X, ℝ)), Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V
+    ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by
+    exact exists_continuous_one_of_compact_subset_open hK pV2 pV1
+  rcases hf with ⟨f, pf1, pf2, pf3⟩
+  calc
+    (μ K).toReal
+        = μ.real K := by rw [measureReal_def]
+      _ = ∫ (x : X), K.indicator 1 x ∂μ :=
+      (integral_indicator_one (μ := μ) (IsCompact.measurableSet hK)).symm
+      _ ≤ ∫ (x : X), (f x : ℝ) ∂μ := by
+        apply integral_mono
+        · apply IntegrableOn.integrable_indicator
+          · apply ContinuousOn.integrableOn_compact hK continuousOn_const
+          · exact IsCompact.measurableSet hK
+        · exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2
+        · intro x
+          classical
+          obtain (hA | hB) := @or_not (x ∈ K)
+          · simp [hA, pf1 hA]
+          · simp [hB, (pf3 x).1]
+      _ = ∫ (x : X), (f x : ℝ) ∂ν := by exact hμν f
+      _ ≤ ∫ (x : X), V.indicator 1 x ∂ν := by
+        apply integral_mono
+        · exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2
+        · apply IntegrableOn.integrable_indicator
+          · apply (integrableOn_const_iff (by finiteness)).mpr
+            exact Or.inr VltTop
+          · exact IsOpen.measurableSet pV2
+        · intro x
+          classical
+          obtain (hA | hB) := @or_not (x ∈ V)
+          · simp [hA, (pf3 x).2]
+          · simp only [hB, not_false_eq_true, Set.indicator_of_notMem]
+            exact le_of_eq (image_eq_zero_of_notMem_tsupport (Set.notMem_subset pf2 hB))
+      _ = ν.real V := integral_indicator_one (IsOpen.measurableSet pV2)
+      _ = (ν V).toReal := by rw [measureReal_def]
+      _ ≤ (ν K).toReal + ↑ε := by
+        rw [ENNReal.toReal, ENNReal.toReal, ← NNReal.coe_add,
+          NNReal.coe_le_coe, ← ENNReal.coe_le_coe, ENNReal.coe_add,
+          ENNReal.coe_toNNReal lem2, ENNReal.coe_toNNReal (ne_of_lt VltTop)]
+        exact pV3
+
+/-- If two regular measures give the same integral for every function in `C_c(X, ℝ)`,
+then they are equal. -/
+theorem eq_of_integral_eq_on_Cc {μ ν : Measure X} [Measure.Regular μ] [Measure.Regular ν]
+    (hμν : ∀ (f : C_c(X, ℝ)), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν) : μ = ν := by
+  apply Measure.OuterRegular.eq_of_eq_on_isOpen
+  apply Measure.InnerRegularWRT.eq_on_q_of_eq_on_p
+  · exact Measure.Regular.innerRegular
+  · exact Measure.Regular.innerRegular
+  · intro K hK
+    apply le_antisymm
+    · exact compare_measure_of_compact_sets hμν K hK
+    · exact compare_measure_of_compact_sets (fun f ↦ (hμν f).symm) K hK
+
+/-- 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, ℝ) →ₚ[ℝ] ℝ := by
+  refine PositiveLinearMap.mk₀ ?_ ?_
+  · refine ⟨⟨fun f ↦ ∫ (x : X), f x ∂μ, ?_⟩, ?_⟩
+    · intro f g
+      simp only [CompactlySupportedContinuousMap.coe_add, Pi.add_apply]
+      refine integral_add' ?_ ?_
+      · exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2
+      · exact Continuous.integrable_of_hasCompactSupport g.1.2 g.2
+    · intro c f
+      simp only [RingHom.id_apply]
+      apply integral_const_mul_of_integrable
+      exact Continuous.integrable_of_hasCompactSupport f.1.2 f.2
+  · intro f hf
+    simp only [LinearMap.coe_mk, AddHom.coe_mk]
+    exact integral_nonneg hf
+
+/-- If two regular measures induce the same positive linear functional on `C_c(X, ℝ)`,
+then they are equal. -/
+theorem eq_of_eq_integralPositiveLinearMap {μ ν : Measure X}
+    [Measure.Regular μ] [Measure.Regular ν]
+    (hμν : integralPositiveLinearMap μ = integralPositiveLinearMap ν) : μ = ν := by
+  apply eq_of_integral_eq_on_Cc
+  intro f
+  simp only [integralPositiveLinearMap, PositiveLinearMap.mk₀, PositiveLinearMap.mk.injEq,
+    LinearMap.mk.injEq, AddHom.mk.injEq] at hμν
+  exact congr_fun hμν f
+
+/-The Riesz measure induced by a positive linear functional on `C_c(X, ℝ)` is regular.-/
+instance rieszMeasure_regular (Λ : C_c(X, ℝ) →ₚ[ℝ] ℝ) : (rieszMeasure Λ).Regular :=
+  Content.regular (rieszContent (CompactlySupportedContinuousMap.toNNRealLinear Λ))
+
+/-- RealRMK.rieszMeasure is a surjective function. That is, every regular measure is induced by a
+positive linear functional on `C_c(X, ℝ)`. -/
+theorem rieszMeasure_surjective {μ : Measure X} [Measure.Regular μ] :
+    μ = rieszMeasure (integralPositiveLinearMap μ) := by
+  apply eq_of_integral_eq_on_Cc
+  intro f
+  trans (integralPositiveLinearMap μ) f
+  · simp [integralPositiveLinearMap]
+    rfl
+  · exact (integral_rieszMeasure (integralPositiveLinearMap μ) f).symm
+
 end RealRMK

Mathlib/MeasureTheory/Measure/Regular.lean

@@ -216,6 +216,18 @@ theorem measure_eq_iSup (H : InnerRegularWRT μ p q) (hU : q U) :
     le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)
   simpa only [lt_iSup_iff, exists_prop] using H hU r hr
 
+theorem eq_on_q_of_eq_on_p {ν : Measure α} (hμ : μ.InnerRegularWRT p q) (hν : ν.InnerRegularWRT p q)
+    (hμν : ∀ U, p U → μ U = ν U) : ∀ U, q U → μ U = ν U := by
+  intro U hU
+  rw [Measure.InnerRegularWRT.measure_eq_iSup hμ hU, Measure.InnerRegularWRT.measure_eq_iSup hν hU]
+  apply iSup_congr
+  intro t
+  apply iSup_congr
+  intro ht1
+  apply iSup_congr
+  intro ht2
+  exact hμν t ht2
+
 theorem exists_subset_lt_add (H : InnerRegularWRT μ p q) (h0 : p ∅) (hU : q U) (hμU : μ U ≠ ∞)
     (hε : ε ≠ 0) : ∃ K, K ⊆ U ∧ p K ∧ μ U < μ K + ε := by
   rcases eq_or_ne (μ U) 0 with h₀ | h₀
@@ -461,6 +473,19 @@ lemma measure_closure_eq_of_isCompact [R1Space α] [OuterRegular μ]
   intro u ku u_open
   exact measure_mono (hk.closure_subset_of_isOpen u_open ku)
 
+/-- Outer regular measures are determined by values on open sets. -/
+theorem eq_of_eq_on_isOpen {ν : Measure α} [OuterRegular μ] [OuterRegular ν]
+    (hμν : ∀ U, IsOpen U → μ U = ν U) : μ = ν := by
+  ext s ms
+  rw [Set.measure_eq_iInf_isOpen, Set.measure_eq_iInf_isOpen]
+  apply iInf_congr
+  intro t
+  apply iInf_congr
+  intro ht1
+  apply iInf_congr
+  intro ht2
+  exact hμν t ht2
+
 end OuterRegular
 
 /-- If a measure `μ` admits finite spanning open sets such that the restriction of `μ` to each set

Mathlib/Topology/UrysohnsLemma.lean

@@ -3,12 +3,12 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Order.Group.Indicator
 import Mathlib.Analysis.Normed.Affine.AddTorsor
 import Mathlib.Analysis.NormedSpace.FunctionSeries
 import Mathlib.Analysis.SpecificLimits.Basic
 import Mathlib.LinearAlgebra.AffineSpace.Ordered
 import Mathlib.Topology.ContinuousMap.Algebra
+import Mathlib.Topology.ContinuousMap.CompactlySupported
 import Mathlib.Topology.GDelta.Basic
 
 /-!
@@ -82,7 +82,7 @@ Urysohn's lemma, normal topological space, locally compact topological space
 
 variable {X : Type*} [TopologicalSpace X]
 
-open Set Filter TopologicalSpace Topology Filter
+open Set Filter TopologicalSpace Topology Filter CompactlySupported
 open scoped Pointwise
 
 namespace Urysohns
@@ -522,6 +522,34 @@ lemma exists_tsupport_one_of_isOpen_isClosed [T2Space X] {s t : Set X}
     apply Urysohns.CU.lim_of_notMem_U
     exact notMem_compl_iff.mpr hx
 
+/-- A variation of Urysohn's lemma. In a Hausdorff locally compact space, for a compact set `K`
+contained in an open set `V`, 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_continuous_one_of_compact_subset_open [T2Space X] [LocallyCompactSpace X]
+    {K V : Set X} (hK : IsCompact K) (hV : IsOpen V) (hKV : K ⊆ V) :
+    ∃ (f : C_c(X, ℝ)), Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by
+  rcases exists_open_between_and_isCompact_closure hK hV hKV with ⟨U, hU1, hU2, hU3, hU4⟩
+  rcases exists_tsupport_one_of_isOpen_isClosed hU1 hU4 (IsCompact.isClosed hK) hU2
+    with ⟨f, hf1, hf2, hf3⟩
+  have : IsCompact (tsupport ⇑f) := by
+    refine IsCompact.of_isClosed_subset hU4 ?_ ?_
+    · apply isClosed_closure
+    · trans U
+      · exact hf1
+      · apply subset_closure
+  use ⟨f, by apply hasCompactSupport_def.mpr this⟩
+  simp only [CompactlySupportedContinuousMap.coe_mk, Set.mem_Icc]
+  constructor <;> try constructor
+  · intro x hx
+    simp only [Pi.one_apply]
+    exact hf2 hx
+  · trans U
+    · exact hf1
+    · trans closure U
+      · apply subset_closure
+      · exact hU3
+  · simp only [Set.mem_Icc] at hf3; intro x; exact hf3 x
+
 theorem exists_continuous_nonneg_pos [RegularSpace X] [LocallyCompactSpace X] (x : X) :
     ∃ f : C(X, ℝ), HasCompactSupport f ∧ 0 ≤ (f : X → ℝ) ∧ f x ≠ 0 := by
   rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩