Filter.limSup and sequence of measures

Stream: new members

[Josha Dekker]

Hi, I'm still trying to get used to the API for filters and measures. In my efforts to formalise the concept of tight measures, I'm trying to prove that a certain alternative characterisation of a tight set of measures implies my chosen characterisation of a tight set of measures (I already have the converse implication, which I've left in for reference).

I know what to do mathematically (see the commented lines), but I cannot seem to get this to work nicely. I'm happy to assume some more structure (e.g. a metric space and things like this), but the less the better!

import Mathlib.MeasureTheory.Measure.Regular

open Topology
open scoped ENNReal

namespace MeasureTheory

variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α}

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

/-- A set `S` of measures is tight if for all `0 < ε`, there exists `K` compact such that for all
`μ` in `S`, `μ Kᶜ ≤ ε`. -/
def IsTightSet [TopologicalSpace α] (S : Set (Measure α)) : Prop :=
  ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

/-- As tight sequences are very common in measuretheory, we encode these in a separate
definition. -/
def IsTightSeq [TopologicalSpace α] (μs : ℕ → Measure α) : Prop :=
  IsTightSet (Set.range fun n => μs n)

lemma limsup [TopologicalSpace α] {μs : ℕ → Measure α} (h : IsTightSeq μs) :
    ∀ ε : ℝ≥0∞, 0 < ε →
    ∃ K : Set α, IsCompact K ∧ Filter.limsup (fun i ↦ (μs i) Kᶜ) Filter.atTop ≤ ε := by
  intro ε hε
  obtain ⟨K, hK, hKμ⟩ := h ε hε
  use K, hK
  apply le_trans Filter.limsup_le_iSup
  exact iSup_le (fun i => hKμ (μs i) (Set.mem_range_self i))

lemma of_limsup [TopologicalSpace α] {μs : ℕ → Measure α} (hs : ∀ n, IsTight (μs n))
    (h : ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, IsCompact K ∧ Filter.limsup (fun i ↦ (μs i) Kᶜ) Filter.atTop ≤ ε) :
    IsTightSeq μs := by
  intro ε hε
  obtain ⟨K', hK', hKμ'⟩ := h ε hε
  sorry
  -- Mathematically:
  --- establish that for some N, i > N implies μs i K'ᶜ ≤ ε
  --- By tightness, extract K_i for each i ≤ N
  --- Let K = (⋃ {i ≤ N}, K_i) ∪ K'
  --- Clearly, K is compact. Also, for all i, μs i Kᶜ ≤ ε

end MeasureTheory

[Kexing Ying]

(deleted) Sorry, I didn't read the assumptions correctly.

[Josha Dekker]

If you can prove it with some more, reasonable, assumptions, I'm more than happy of course. It feels like this should need only very little (perhaps something to let the limsup work nicely), but I may be wrong (I'm still trying to wrap my head around using filters in measure theory)

[Kexing Ying]

I think the lemma you want is eventually_lt_of_limsup_lt and eventually_atTop. Also you can use the tactic choose to to find the sequence of compact sets from assumption hs: something like choose K hK₁ hK₂ using hs

[Josha Dekker]

thanks, I think that pointed me in the right direction, I've almost completed the proof now! I'll post the finished version here once I'm ready!

[Vincent Beffara]

Ah that reminds me, do we have somewhere a version of limsup for functions with values in \R, where the limsup is in EReal? In many cases it would be nicer to use than carrying around IsBoundedUnder asumptions...

[Josha Dekker]

I still need to golf this (if you like, have fun....), but I managed to complete the proof!

import Mathlib.MeasureTheory.Measure.Regular

open Topology
open scoped ENNReal

namespace MeasureTheory

variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α}

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

/-- A set `S` of measures is tight if for all `0 < ε`, there exists `K` compact such that for all
`μ` in `S`, `μ Kᶜ ≤ ε`. -/
def IsTightSet [TopologicalSpace α] (S : Set (Measure α)) : Prop :=
  ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε

/-- As tight sequences are very common in measuretheory, we encode these in a separate
definition. -/
def IsTightSeq [TopologicalSpace α] (μs : ℕ → Measure α) : Prop :=
  IsTightSet (Set.range fun n => μs n)

lemma limsup [TopologicalSpace α] {μs : ℕ → Measure α} (h : IsTightSeq μs) :
    ∀ ε : ℝ≥0∞, 0 < ε →
    ∃ K : Set α, IsCompact K ∧ Filter.limsup (fun i ↦ (μs i) Kᶜ) Filter.atTop ≤ ε := by
  intro ε hε
  obtain ⟨K, hK, hKμ⟩ := h ε hε
  use K, hK
  apply le_trans Filter.limsup_le_iSup
  exact iSup_le (fun i => hKμ (μs i) (Set.mem_range_self i))

lemma of_limsup [TopologicalSpace α] {μs : ℕ → Measure α} (hs : ∀ n, IsTight (μs n))
    (h : ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, IsCompact K ∧ Filter.limsup (fun i ↦ (μs i) Kᶜ) Filter.atTop ≤ ε) :
    IsTightSeq μs := by
  intro ε hε
  by_cases hε_fin : ε < ∞
  · have hε2 : 0 < ε / 2 := ENNReal.half_pos hε.ne'
    obtain ⟨K', hK', hKμ'⟩ := h (ε / 2) hε2
    have hKμ' : Filter.limsup (fun i ↦ (μs i) K'ᶜ) Filter.atTop < ε := by
      apply lt_of_le_of_lt hKμ' (ENNReal.half_lt_self hε.ne' hε_fin.ne'.symm)
    have := Filter.eventually_lt_of_limsup_lt hKμ'
    rw [Filter.eventually_atTop] at this
    obtain ⟨N, hN⟩ := this
    choose K hK₁ hK₂ using fun n => hs n ε hε
    use (⋃ (i ≤ N), K i) ∪ K'
    constructor
    · apply IsCompact.union
      · exact Set.Finite.isCompact_biUnion (Set.finite_le_nat N) (fun i hi => hK₁ i)
      · exact hK'
    · intro μ hy
      simp only [Set.mem_range] at hy
      obtain ⟨n, hn⟩ := hy
      by_cases hnN : n ≤ N
      · have : μ (K n)ᶜ ≤ ε := by
          rw [← hn]
          apply hK₂
        apply le_trans (measure_mono ?_) this
        rw [Set.compl_subset_compl]
        apply Set.subset_union_of_subset_left
        exact Set.subset_biUnion_of_mem hnN
      · have : μ (K')ᶜ ≤ ε := by
          rw [← hn]
          exact (hN n (Nat.le_of_not_ge hnN)).le
        apply le_trans (measure_mono ?_) this
        rw [Set.compl_subset_compl]
        apply Set.subset_union_of_subset_right
        rfl
  · use ∅, isCompact_empty
    intro μ_1 _
    simp_all only [not_lt, top_le_iff, Set.mem_range, Set.compl_empty, le_top]

end MeasureTheory

[Josha Dekker]

Thank you for your help!

[Josha Dekker]

I golved it a bit, might golf it a bit more later!

lemma of_limsup [TopologicalSpace α] {μs : ℕ → Measure α} (hs : ∀ n, IsTight (μs n))
    (h : ∀ ε : ℝ≥0∞, 0 < ε →
      ∃ K : Set α, IsCompact K ∧ Filter.limsup (fun i ↦ (μs i) Kᶜ) Filter.atTop ≤ ε) :
    IsTightSeq μs := by
  intro ε hε
  by_cases hε_fin : ε < ∞
  · obtain ⟨K', hK', hKμ'⟩ := h (ε / 2) (ENNReal.half_pos hε.ne')
    obtain ⟨N, hN⟩ := Filter.eventually_atTop.mp (Filter.eventually_lt_of_limsup_lt
      (lt_of_le_of_lt hKμ' (ENNReal.half_lt_self hε.ne' hε_fin.ne'.symm)))
    choose K hK₁ hK₂ using fun n => hs n ε hε
    use (⋃ (i ≤ N), K i) ∪ K'
    constructor
    · exact IsCompact.union ((Set.finite_le_nat N).isCompact_biUnion (fun i _ => hK₁ i)) hK'
    · intro μ hy
      obtain ⟨n, hn⟩ := Set.mem_range.mp hy
      rw [← hn]
      by_cases hnN : n ≤ N
      · apply le_trans (measure_mono ?_) (hK₂ n)
        rw [Set.compl_subset_compl]
        apply Set.subset_union_of_subset_left
        exact Set.subset_biUnion_of_mem hnN
      · apply le_trans (measure_mono ?_) (hN n (Nat.le_of_not_ge hnN)).le
        rw [Set.compl_subset_compl]
        apply Set.subset_union_of_subset_right
        rfl
  · use ∅, isCompact_empty
    intro μ _
    simp_all only [not_lt, top_le_iff, Set.mem_range, Set.compl_empty, le_top]

[Kexing Ying]

Vincent Beffara said:

Ah that reminds me, do we have somewhere a version of limsup for functions with values in \R, where the limsup is in EReal? In many cases it would be nicer to use than carrying around IsBoundedUnder asumptions...

I don't think so. It does seem very useful since I remember being bit by IsBoundedUnder. But I guess introducing this definition will require the duplication of a lot of lemmas.

[Sébastien Gouëzel]

Just write this as the limsup of the composition of your original function with the coercion from reals to ereals?

[Vincent Beffara]

Yep the definition is clear but some API around it would help.

[Vincent Beffara]

Mostly linking boundedness to finite values I guess