Subspaces, topological and measurable properties

Stream: new members

[Josha Dekker]

Hi, I have one more result I would like to include before submitting my definitions of tightness of measures, which is in a sense a consequence of the Ulam tightness theorem. However, I'm struggling with how to pass to a subspace here (and back...). What is the proper way to approach this?

import Mathlib.MeasureTheory.Measure.Regular
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.Measure.Portmanteau

open Topology Filter Uniformity Uniform MeasureTheory Set
open scoped ENNReal

namespace MeasureTheory

variable {α ι : Type*}

variable [MeasurableSpace α] {μ : Measure α}

/-- A measure `μ` is separable if there is a separable set `S` such that `μ S = μ Set.univ`. -/
 def IsSeparable [TopologicalSpace α] (μ : Measure α) : Prop :=
   ∃ S : Set α, TopologicalSpace.IsSeparable S ∧ μ S = μ Set.univ

/-- A measure `μ` is pre-tight if for all `0 < ε`, there exists `K` totally bounded such that
  `μ Kᶜ ≤ ε`. -/
def IsPretight [UniformSpace α] (μ : Measure α) : Prop :=
  ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, TotallyBounded K ∧ μ Kᶜ ≤ ε

/-- Ulam tightness theorem, which I have already proven. -/
lemma of_separableSpace_on_metric [PseudoMetricSpace α] [TopologicalSpace.SeparableSpace α]
    [OpensMeasurableSpace α] [IsFiniteMeasure μ] : IsPretight μ := by
  sorry

-- The proof idea is simple: if `μ` is separable, then there exists a separable set `S` such that
-- `μ S = μ Set.univ`. On the subspace (closure S) we can invoke `of_separableSpace_on_metric` to get that
-- `μ` is pre-tight on this subspace. As this has full measure, we want to lift this back.
lemma of_isSeparable_on_metric [PseudoMetricSpace α] [OpensMeasurableSpace α]
    (h : IsSeparable μ) [IsFiniteMeasure μ] : IsPretight μ := by
  obtain ⟨S, hS, hSμ⟩ := h
  have : TopologicalSpace.PseudoMetrizableSpace (closure S) := by
    infer_instance
  have : TopologicalSpace.SeparableSpace (closure S) := by
    have hSc := TopologicalSpace.IsSeparable.closure hS
    have : closure S = Set.univ (α := closure S) := by
      exact (Subtype.coe_image_univ (closure S)).symm
    rw [this] at hSc
    sorry
  have := of_separableSpace_on_metric (α := closure S) -- fails

[Josha Dekker]

Does anyone have pointers on this? I tried proving the result directly by adapting my proof of the Ulam tightness theorem, but for the necessary auxiliary results, I ended up with even more subtyping problems, so I don't think that is the way to go... I believe the above should be able to work, but I'm too inexperienced with subtypes to get it to work

[Josha Dekker]

If you like more context, this is the last thing I need in #12394 (other than cleaning up / moving some of the auxiliary results)

[Luigi Massacci]

can’t you “manually” make the MeasureSpace instance using something like docs#Subtype.opensMeasurableSpace ?

[Luigi Massacci]

But if you want to avoid subtypes it’s probably not the right approach

[Josha Dekker]

Thank you for your suggestion! I'd like to use the result that I have proven (if possible) to prove the result I still have open. If you think that it is better to work via subtypes, I'm happy to try this. However, I'm getting a new TC problem here:

-- The proof idea is simple: if `μ` is separable, then there exists a separable set `S` such that
-- `μ S = μ Set.univ`. On the subspace (closure S) we can invoke `of_separableSpace_on_metric` to
-- get that `μ` is pre-tight on this subspace. As this has full measure, we want to lift this back.
lemma of_isSeparable_on_metric [PseudoMetricSpace α] [OpensMeasurableSpace α]
    (h : IsSeparable μ) [IsFiniteMeasure μ] : IsPretight μ := by
  obtain ⟨S, hS, hSμ⟩ := h
  have : TopologicalSpace.PseudoMetrizableSpace (closure S) := by
    infer_instance
  have : TopologicalSpace.SeparableSpace (closure S) := by
    have hSc := TopologicalSpace.IsSeparable.closure hS
    have : closure S = Set.univ (α := closure S) := by
      exact (Subtype.coe_image_univ (closure S)).symm
    rw [this] at hSc
    sorry
  have mα : MeasureSpace α := by
    exact ⟨μ⟩
  have := Subtype.opensMeasurableSpace (closure S)
  have : MeasureSpace (closure S) := by
    exact Measure.Subtype.measureSpace
  have := of_separableSpace_on_metric (μ := this.volume) -- fails with
    --synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
    --Subtype.instMeasurableSpace
    --inferred
    --MeasureSpace.toMeasurableSpace
  sorry

[Josha Dekker]

An alternative approach would be to prove my auxiliary results for subtypes all the way, although I expect that to face similar problems...

[Luigi Massacci]

What happens if you swaps the have-s with let-s? That might work

[Josha Dekker]

Thank you, this is actually getting me very close (a bit sloppy still). I have three sorry's left, where I think the second and third require some way of relating volume back to my measure μ that I'm not aware of.

-- The proof idea is simple: if `μ` is separable, then there exists a separable set `S` such that
-- `μ S = μ Set.univ`. On the subspace (closure S) we can invoke `of_separableSpace_on_metric` to
-- get that `μ` is pre-tight on this subspace. As this has full measure, we want to lift this back.
lemma of_isSeparable_on_metric [PseudoMetricSpace α] [OpensMeasurableSpace α]
    (h : IsSeparable μ) [IsFiniteMeasure μ] : IsPretight μ := by
  obtain ⟨S, hS, hSμ⟩ := h
  letI : TopologicalSpace.PseudoMetrizableSpace (closure S) := by
    infer_instance
  letI : TopologicalSpace.SeparableSpace (closure S) := by
    have hSc := TopologicalSpace.IsSeparable.closure hS
    have : closure S = Set.univ (α := closure S) := by
      exact (Subtype.coe_image_univ (closure S)).symm
    rw [this] at hSc
    sorry
  letI mα : MeasureSpace α := by
    exact ⟨μ⟩
  letI := Subtype.opensMeasurableSpace (closure S)
  letI mS : MeasureSpace (closure S) := by
    exact Measure.Subtype.measureSpace
  letI : IsFiniteMeasure mS.volume := by
    refine { measure_univ_lt_top := ?_ }
    have : μ (Set.univ) < ⊤ := by
      exact IsFiniteMeasure.measure_univ_lt_top
    apply lt_of_le_of_lt ?_ this
    simp at *
    sorry
  letI := of_separableSpace_on_metric (μ := mS.volume)
  intro ε hε
  obtain ⟨K, hK, hKe⟩ := this ε hε
  use K
  constructor
  · rw [Metric.totallyBounded_iff] at *
    intro δ hδ
    obtain ⟨N, hN⟩ := hK δ hδ
    use N, Finite.image Subtype.val hN.1
    aesop
  · sorry

[Luigi Massacci]

Here is the second one:

  letI : IsFiniteMeasure mS.volume := by
    constructor
    rw [Measure.Subtype.volume_univ (MeasurableSet.nullMeasurableSet measurableSet_closure)]
    exact measure_lt_top volume (closure S)

and for the third one let me actually read your definition of pre-tight measure, I'm giving measure theory this semester so I have never heard of it yet : )

[Josha Dekker]

Luigi Massacci said:

Here is the second one:

  letI : IsFiniteMeasure mS.volume := by
    constructor
    rw [Measure.Subtype.volume_univ (MeasurableSet.nullMeasurableSet measurableSet_closure)]
    exact measure_lt_top volume (closure S)

and for the third one let me actually read your definition of pre-tight measure, I'm giving measure theory this semester so I have never heard of it yet : )

Thank you! I think pre-tight measures are not particularly beautiful, as they depend on the metric space structure of the space. However, getting a totally bounded set can sometimes be useful

[Luigi Massacci]

Here is the first one:

  letI : TopologicalSpace.SeparableSpace (closure S) := by
    exact TopologicalSpace.IsSeparable.separableSpace <| TopologicalSpace.IsSeparable.closure hS

[Josha Dekker]

Luigi Massacci said:

Here is the first one:

  letI : TopologicalSpace.SeparableSpace (closure S) := by
    exact TopologicalSpace.IsSeparable.separableSpace <| TopologicalSpace.IsSeparable.closure hS

Thank you! The remaining sorry (after applying apply le_trans ?_ hKe) becomes ↑↑μ (Subtype.val '' K)ᶜ ≤ ↑↑volume Kᶜ, which I guess should be independent of the definition of pre-tight.

[Josha Dekker]

Luigi Massacci said:

Here is the first one:

  letI : TopologicalSpace.SeparableSpace (closure S) := by
    exact TopologicalSpace.IsSeparable.separableSpace <| TopologicalSpace.IsSeparable.closure hS

So I think the crucial aspect that needs to be included here is hSμ, the fact that the measure concentrates on the set S, as the two complements do not necessarily align well. Or the problem is in relating volume to this measure, which I'm not sure of how to proceed either.

[Luigi Massacci]

Ok so this is indeed non-obvious even ignoring the lean aspects (at least to me), this way (which I think is good?) you get rid of your subtyping problems and are working only in the bigger space:

  · apply le_trans ?_ hKe
    rw [Measure.Subtype.volume_def]
    rw [MeasureTheory.Measure.comap_apply _ Subtype.val_injective]
    · sorry
    · intro s hs
      refine MeasurableSet.subtype_image ?refine_1.h.hs hs
      apply measurableSet_closure
    · sorry

[Josha Dekker]

Thank you! By replacing K by closure K, we can clear the last sorry, so the current proof is given below. I think I'm very close, rewriting 'volume' helps a bit

-- The proof idea is simple: if `μ` is separable, then there exists a separable set `S` such that
-- `μ S = μ Set.univ`. On the subspace (closure S) we can invoke `of_separableSpace_on_metric` to
-- get that `μ` is pre-tight on this subspace. As this has full measure, we want to lift this back.
lemma of_isSeparable_on_metric [PseudoMetricSpace α] [OpensMeasurableSpace α]
    (h : IsSeparable μ) [IsFiniteMeasure μ] : IsPretight μ := by
  obtain ⟨S, hS, hSμ⟩ := h
  letI : TopologicalSpace.SeparableSpace (closure S) := by
    exact TopologicalSpace.IsSeparable.separableSpace <| TopologicalSpace.IsSeparable.closure hS
  letI mα : MeasureSpace α := ⟨μ⟩
  --letI := Subtype.opensMeasurableSpace (closure S)
  letI mS : MeasureSpace (closure S) := Measure.Subtype.measureSpace
  letI : IsFiniteMeasure mS.volume := by
    constructor
    rw [Measure.Subtype.volume_univ (MeasurableSet.nullMeasurableSet measurableSet_closure)]
    exact measure_lt_top volume (closure S)
  letI := of_separableSpace_on_metric (μ := mS.volume)
  intro ε hε
  obtain ⟨K, hK, hKe⟩ := this ε hε
  have hSμ : μ (closure S) = μ Set.univ := le_antisymm (measure_mono <| Set.subset_univ _)
    (le_trans hSμ.ge (measure_mono <| subset_closure))
  use (closure K)
  constructor
  · apply TotallyBounded.closure
    rw [Metric.totallyBounded_iff] at *
    intro δ hδ
    obtain ⟨N, hN⟩ := hK δ hδ
    use N, Finite.image Subtype.val hN.1
    simp_all only [iUnion_coe_set, mem_image, Subtype.exists, exists_and_right, exists_eq_right,
      iUnion_exists, image_subset_iff, preimage_iUnion]
    exact hN.right
  · have hKe : volume (closure K)ᶜ ≤ ε := by
      apply le_trans ?_ hKe
      apply measure_mono
      rw [Set.compl_subset_compl]
      exact subset_closure
    apply le_trans ?_ hKe
    rw [Measure.Subtype.volume_def]
    rw [MeasureTheory.Measure.comap_apply _ Subtype.val_injective]
    · rw [volume]
      simp only
      apply measure_mono
      sorry

    · intro s hs
      refine MeasurableSet.subtype_image ?refine_1.h.hs hs
      apply measurableSet_closure
    · measurability

[Josha Dekker]

I still need to clean it up a bit more, but I'm now down to one (mathematically) trivial claim, so I think I should be able to handle it! Thanks a lot for all the help!

-- The proof idea is simple: if `μ` is separable, then there exists a separable set `S` such that
-- `μ S = μ Set.univ`. On the subspace (closure S) we can invoke `of_separableSpace_on_metric` to
-- get that `μ` is pre-tight on this subspace. As this has full measure, we want to lift this back.
lemma of_isSeparable_on_metric [PseudoMetricSpace α] [OpensMeasurableSpace α]
    (h : IsSeparable μ) [IsFiniteMeasure μ] : IsPretight μ := by
  obtain ⟨S, hS, hSμ⟩ := h
  letI : TopologicalSpace.SeparableSpace (closure S) := by
    exact TopologicalSpace.IsSeparable.separableSpace <| TopologicalSpace.IsSeparable.closure hS
  letI mα : MeasureSpace α := ⟨μ⟩
  --letI := Subtype.opensMeasurableSpace (closure S)
  letI mS : MeasureSpace (closure S) := Measure.Subtype.measureSpace
  letI : IsFiniteMeasure mS.volume := by
    constructor
    rw [Measure.Subtype.volume_univ (MeasurableSet.nullMeasurableSet measurableSet_closure)]
    exact measure_lt_top volume (closure S)
  letI := of_separableSpace_on_metric (μ := mS.volume)
  intro ε hε
  obtain ⟨K, hK, hKe⟩ := this ε hε
  have hSμ : μ (closure S) = μ Set.univ := le_antisymm (measure_mono <| Set.subset_univ _)
    (le_trans hSμ.ge (measure_mono <| subset_closure))
  use (closure K)
  constructor
  · apply TotallyBounded.closure
    rw [Metric.totallyBounded_iff] at *
    intro δ hδ
    obtain ⟨N, hN⟩ := hK δ hδ
    use N, Finite.image Subtype.val hN.1
    simp_all only [iUnion_coe_set, mem_image, Subtype.exists, exists_and_right, exists_eq_right,
      iUnion_exists, image_subset_iff, preimage_iUnion]
    exact hN.right
  · have hKe : volume (closure K)ᶜ ≤ ε := by
      apply le_trans ?_ hKe
      apply measure_mono
      rw [Set.compl_subset_compl]
      exact subset_closure
    apply le_trans ?_ hKe
    rw [Measure.Subtype.volume_def]
    rw [MeasureTheory.Measure.comap_apply _ Subtype.val_injective]
    · rw [← MeasureTheory.measure_inter_add_diff₀ (t := closure S)]
      rw [← MeasureTheory.measure_inter_add_diff₀ (μ := volume) (t := closure S)]
      rw [volume]
      simp only
      congr
      apply add_le_add
      · apply measure_mono
        intro x hx
        simp [closure_subtype, Subtype.val_inj]
        constructor
        · simp_all only [mem_inter_iff, mem_compl_iff, not_false_eq_true]
        · simp_all only [mem_inter_iff, mem_compl_iff]
      · sorry
      · apply MeasurableSet.nullMeasurableSet
        measurability
      · apply MeasurableSet.nullMeasurableSet
        measurability
    · intro s hs
      refine MeasurableSet.subtype_image ?refine_1.h.hs hs
      apply measurableSet_closure
    · measurability

[Luigi Massacci]

My pleasure

[Josha Dekker]

Luigi Massacci said:

My pleasure

I ended up with this for now, I'm afraid I can't really break down the length much more without introducing many intermediate results, so I'll see what comes up in review!

-- The proof idea is simple: if `μ` is separable, then there exists a separable set `S` such that
-- `μ S = μ Set.univ`. On the subspace (closure S) we can invoke `of_separableSpace_on_metric` to
-- get that `μ` is pre-tight on this subspace. As this has full measure, we want to lift this back.
lemma of_isSeparable_on_metric [PseudoMetricSpace α] [OpensMeasurableSpace α]
    (h : IsSeparable μ) [IsFiniteMeasure μ] : IsPretight μ := by
  obtain ⟨S, hS, hSμ⟩ := h
  have : TopologicalSpace.SeparableSpace (closure S) :=
    TopologicalSpace.IsSeparable.separableSpace <| TopologicalSpace.IsSeparable.closure hS
  letI mα : MeasureSpace α := ⟨μ⟩
  letI mS : MeasureSpace (closure S) := Measure.Subtype.measureSpace
  have : IsFiniteMeasure mS.volume := by
    constructor
    rw [Measure.Subtype.volume_univ (MeasurableSet.nullMeasurableSet measurableSet_closure)]
    exact measure_lt_top volume (closure S)
  have := of_separableSpace_on_metric (μ := mS.volume)
  intro ε hε
  obtain ⟨K, hK, hKe⟩ := this ε hε
  have hSμ : μ (closure S) = μ Set.univ := le_antisymm (measure_mono <| Set.subset_univ _)
    (le_trans hSμ.ge (measure_mono <| subset_closure))
  have hSμ_co : μ (closure S)ᶜ = 0 := by
    rw [MeasureTheory.measure_compl, tsub_eq_zero_of_le hSμ.ge]
    · measurability
    · rw [hSμ]
      exact measure_ne_top _ _
  use (closure K)
  constructor
  · apply TotallyBounded.closure
    rw [Metric.totallyBounded_iff] at *
    intro δ hδ
    obtain ⟨N, hN⟩ := hK δ hδ
    use N, Finite.image Subtype.val hN.1
    simp_all only [iUnion_coe_set, mem_image, Subtype.exists, exists_and_right, exists_eq_right,
      iUnion_exists, image_subset_iff, preimage_iUnion]
    exact hN.right
  · have hKe : volume (closure K)ᶜ ≤ ε := by
      apply le_trans ?_ hKe
      apply measure_mono
      rw [Set.compl_subset_compl]
      exact subset_closure
    apply le_trans ?_ hKe
    rw [Measure.Subtype.volume_def, MeasureTheory.Measure.comap_apply _ Subtype.val_injective]
    · rw [← MeasureTheory.measure_inter_add_diff₀ (t := closure S),
        ← MeasureTheory.measure_inter_add_diff₀ (μ := volume) (t := closure S), volume]
      congr
      apply add_le_add
      · apply measure_mono
        intro x hx
        simp only [mem_inter_iff, mem_image, mem_compl_iff, closure_subtype, Subtype.exists,
          exists_and_left, exists_prop, exists_eq_right_right, and_self_right]
        constructor <;> simp_all only [mem_inter_iff, mem_compl_iff, not_false_eq_true]
      · have : μ ((closure (Subtype.val '' K))ᶜ \ closure S) = 0 := by
          rw [← nonpos_iff_eq_zero, ← hSμ_co]
          apply measure_mono
          intro x hx
          simp_all only [mem_diff, mem_compl_iff, not_false_eq_true]
        rw [this]
        exact zero_le _
      · apply MeasurableSet.nullMeasurableSet
        measurability
      · apply MeasurableSet.nullMeasurableSet
        measurability
    · exact fun s hs ↦ MeasurableSet.subtype_image measurableSet_closure hs
    · measurability

[Josha Dekker]

I'll post my message from a different thread here as well, as it relates to this thread:

Hi, #12394 is up for review and defines IsSeparable, IsPretight and IsTight and shows some relationships between them. Main result is Ulam's tightness theorem (and a strengthened version that only requires IsSeparable rather than SeparableSpace. It is still building, but I don't expect any problems there! I think most results are straightforward, although some proofs are a bit longish: I've used 4 private lemma's to break up the work a bit, but still Ulam's tightness theorem and its strengthened form require some legwork.