For measures, is MutuallySingular the same as Disjoint?

Stream: maths

[Rémy Degenne]

The definition MeasureTheory.Measure.MutuallySingular seems very close to Disjoint for measures.

Below is a (probably very golfable) proof that they are actually equivalent for sigma-finite measures. How about other measures? Does the equivalence break for s-finite measures? Are they always equivalent? If they are, should we drop the MutuallySingular definition?

import Mathlib

open MeasureTheory Set
open scoped ENNReal

variable {α : Type*} [MeasurableSpace α] {μ ν : Measure α}

lemma withDensity_mono_measure (h : μ ≤ ν) (f : α → ℝ≥0∞) : μ.withDensity f ≤ ν.withDensity f := by
  refine Measure.le_intro fun s hs _ ↦ ?_
  rw [withDensity_apply _ hs, withDensity_apply _ hs]
  exact lintegral_mono_fn' (fun _ ↦ le_rfl) (Measure.restrict_mono subset_rfl h)

lemma disjoint_of_mutuallySingular (h : μ ⟂ₘ ν) : Disjoint μ ν := by
  have h_bot_iff (ξ : Measure α) : ξ ≤ ⊥ ↔ ξ = 0 := by
      rw [le_bot_iff]
      rfl
  intro ξ hξμ hξν
  rw [h_bot_iff]
  ext s hs
  simp only [Measure.coe_zero, Pi.zero_apply]
  rw [← inter_union_compl s h.nullSet, measure_union, add_eq_zero]
  · constructor
    · refine measure_inter_null_of_null_right _ ?_
      exact Measure.absolutelyContinuous_of_le hξμ h.measure_nullSet
    · refine measure_inter_null_of_null_right _ ?_
      exact Measure.absolutelyContinuous_of_le hξν h.measure_compl_nullSet
  · exact Disjoint.mono inter_subset_right inter_subset_right disjoint_compl_right
  · exact hs.inter h.measurableSet_nullSet.compl

lemma mutuallySingular_of_disjoint [SigmaFinite μ] [SigmaFinite ν] (h : Disjoint μ ν) :
    μ ⟂ₘ ν := by
  have h_bot_iff (ξ : Measure α) : ξ ≤ ⊥ ↔ ξ = 0 := by
      rw [le_bot_iff]
      rfl
  let p := μ.rnDeriv (μ + ν)
  have hp : Measurable p := Measure.measurable_rnDeriv _ _
  let q := ν.rnDeriv (μ + ν)
  have hq : Measurable q := Measure.measurable_rnDeriv _ _
  have hμ_eq : μ = (μ + ν).withDensity p := by
    refine (Measure.withDensity_rnDeriv_eq μ (μ + ν) ?_).symm
    exact Measure.absolutelyContinuous_of_le (Measure.le_add_right le_rfl)
  have hν_eq : ν = (μ + ν).withDensity q := by
    refine (Measure.withDensity_rnDeriv_eq ν (μ + ν) ?_).symm
    exact Measure.absolutelyContinuous_of_le (Measure.le_add_left le_rfl)
  let ξ := (μ + ν).withDensity (p * q)
  have hξ : ξ ≤ ⊥ := by
    refine h ?_ ?_
    · unfold ξ
      rw [← mul_comm, MeasureTheory.withDensity_mul _ hq hp]
      calc ((μ + ν).withDensity q).withDensity p
      _ ≤ ν.withDensity p := withDensity_mono_measure (Measure.withDensity_rnDeriv_le _ _) _
      _ ≤ (μ + ν).withDensity p := withDensity_mono_measure (Measure.le_add_left le_rfl) _
      _ ≤ μ := Measure.withDensity_rnDeriv_le _ _
    · unfold ξ
      rw [MeasureTheory.withDensity_mul _ hp hq]
      calc ((μ + ν).withDensity p).withDensity q
      _ ≤ μ.withDensity q := withDensity_mono_measure (Measure.withDensity_rnDeriv_le _ _) _
      _ ≤ (μ + ν).withDensity q := withDensity_mono_measure (Measure.le_add_right le_rfl) _
      _ ≤ ν := Measure.withDensity_rnDeriv_le _ _
  rw [← Measure.singularPart_eq_self]
  suffices μ.rnDeriv ν =ᵐ[ν] 0 by
    conv_rhs => rw [Measure.haveLebesgueDecomposition_add μ ν]
    rw [withDensity_congr_ae this]
    simp
  have h_eq : ((μ + ν).withDensity p).rnDeriv ν =ᵐ[ν] fun x ↦ p x * (μ + ν).rnDeriv ν x :=
    Measure.rnDeriv_withDensity_left (ν := ν) hp.aemeasurable (Measure.rnDeriv_ne_top μ (μ + ν))
  rw [← hμ_eq] at h_eq
  refine h_eq.trans ?_
  rw [hν_eq, Filter.EventuallyEq, ae_withDensity_iff hq]
  suffices p * q =ᵐ[μ + ν] 0 by
    filter_upwards [this] with x hx
    simp only [Pi.mul_apply, Pi.zero_apply, mul_eq_zero] at hx
    cases hx with
    | inl h => simp [h]
    | inr h => simp [h]
  rw [← withDensity_eq_zero_iff]
  swap; · exact (hp.mul hq).aemeasurable
  rw [← h_bot_iff]
  exact hξ

[Rémy Degenne]

The proof I wrote needs the sigma-finite assumption only to go from disjoint to mutually singular. The other direction is true for all measures.

[Yury G. Kudryashov]

At least, this is true for s-finite measures: both conditions are equivalent to rnDeriv being a.e. zero.

[Yury G. Kudryashov]

(or do I need 1 of the measures to be sigma-finite for this proof?)

[Rémy Degenne]

That's the main idea of what I prove above: the R.N. derivatives are zero. Sigma-finite is needed by at least one of the lemmas I used. There are several possibilities and I did not have the time to investigate yet which of them is true:
1) that proof really needs sigma-finite
2) the equivalence to rnDeriv being zero is true more generally and I took a wrong turn somewhere
3) one of the lemmas I used is not written in the right generality. A lot of code about rnDeriv was written before we introduced s-finite and could still be using sigma-finite instead.
I will return to the question in a few days, but I wanted to also post here in case someone could help.

[Kexing Ying]

Here's a almost complete proof (Here Measure.inf is a bona-fide measure as can be seen from here):

import Mathlib

namespace MeasureTheory

open ENNReal Set

variable {α} {_ : MeasurableSpace α} {μ ν : Measure α}

noncomputable
def Measure.inf (μ ν : Measure α) : Measure α :=
  ofMeasurable
    (fun s hs ↦ sInf {m | ∃ (t : Set α) (ht : MeasurableSet t),
      m = μ (t ∩ s) + ν (tᶜ ∩ s)})
    sorry sorry

lemma Measure.inf_apply {s : Set α} (hs : MeasurableSet s) :
    μ.inf ν s = sInf {m | ∃ (t : Set α) (_ : MeasurableSet t), m = μ (t ∩ s) + ν (tᶜ ∩ s)} :=
  ofMeasurable_apply s hs

lemma Measure.inf_symm : μ.inf ν = ν.inf μ := by
  refine Measure.ext fun s hs ↦ ?_
  rw [Measure.inf_apply hs, Measure.inf_apply hs]
  congr
  ext m
  exact ⟨fun ⟨t, ht₁, ht₂⟩ ↦ ⟨tᶜ, ht₁.compl, by rwa [compl_compl, add_comm]⟩,
    fun ⟨t, ht₁, ht₂⟩ ↦ ⟨tᶜ, ht₁.compl, by rwa [compl_compl, add_comm]⟩⟩

lemma Measure.inf_le_left (μ ν : Measure α) : μ.inf ν ≤ μ := by
  refine Measure.le_intro <| fun s hs _ ↦ ?_
  rw [Measure.inf_apply hs]
  exact sInf_le ⟨s, hs, by simp⟩

lemma Measure.inf_le_right (μ ν : Measure α) : μ.inf ν ≤ ν := by
  rw [Measure.inf_symm]
  exact Measure.inf_le_left ν μ

lemma aux₁ {s : Set ℝ≥0∞} (h : s.Nonempty) (hs : sInf s = 0) (n : ℕ) {ε : ℝ≥0∞} (hε : 0 < ε) :
    ∃ x ∈ s, x < ε * (1 / 2) ^ n :=
  exists_lt_of_csInf_lt h <| hs ▸ ENNReal.mul_pos hε.ne.symm (by simp)

lemma aux₂ {x : ℝ≥0∞} {ε : ℝ≥0∞}
    (h : ∀ n : ℕ, x ≤ ε * (1 / 2) ^ n) : x = 0 := by
  sorry

lemma aux₃ {ε : ℝ≥0∞} (hε : 0 < ε) : ∑' (n : ℕ), ε * (1 / 2) ^ n = 2 * ε := by
  sorry

lemma Disjoint.mutuallySingular' (h : Disjoint μ ν) (ε : ℝ≥0∞) (hε : 0 < ε) :
    ∃ (s : Set α) (_ : MeasurableSet s), μ s = 0 ∧ ν sᶜ ≤ 2 * ε := by
  specialize h (μ.inf_le_left ν) (μ.inf_le_right ν)
  have h₁ : μ.inf ν univ = 0 := le_bot_iff.1 h ▸ rfl
  simp_rw [Measure.inf_apply MeasurableSet.univ, inter_univ] at h₁
  have h₂ : ∀ n : ℕ, ∃ t : Set α, MeasurableSet t ∧ μ t + ν tᶜ < ε * (1 / 2) ^ n := by
    intro n
    have hn : {m | ∃ (t : Set α) (_ : MeasurableSet t), m = μ t + ν tᶜ}.Nonempty :=
      ⟨ν univ, ∅, MeasurableSet.empty, by simp⟩
    obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ := aux₁ hn h₁ n hε
    exact ⟨t, ht₁, hm₂⟩
  choose t ht₁ ht₂ using h₂
  refine ⟨⋂ n, t n, MeasurableSet.iInter ht₁, ?_, ?_⟩
  · refine aux₂ <| fun n ↦ ((measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans
      (le_add_right le_rfl)).trans (ht₂ n).le
  · rw [compl_iInter]
    refine (measure_iUnion_le _).trans (aux₃ hε ▸ ?_)
    exact tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
      ENNReal.summable ENNReal.summable

lemma Disjoint.mutuallySingular'' (h : Disjoint μ ν) (n : ℕ) :
    ∃ (s : Set α) (_ : MeasurableSet s), μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n := by
  have := Disjoint.mutuallySingular' h ((1 / 2) ^ (n + 1))
    <| ENNReal.pow_pos (by simp) (n + 1)
  convert this
  rw [pow_succ, ← mul_assoc, mul_comm, ← mul_assoc, ENNReal.div_mul_cancel, one_mul]
  simp
  simp

lemma Disjoint.mutuallySingular (h : Disjoint μ ν) :
    μ ⟂ₘ ν := by
  choose s hs₁ hs₂ hs₃ using Disjoint.mutuallySingular'' h
  refine ⟨⋃ n, s n, MeasurableSet.iUnion hs₁, measure_iUnion_null hs₂, ?_⟩
  rw [compl_iUnion]
  refine aux₂ (ε := 1) <| fun n ↦ ?_
  rw [one_mul]
  exact (measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)

end MeasureTheory

[Rémy Degenne]

Great, thanks! I guess your inf is the same as the inf in our complete lattice instance? MeasureTheory.Measure.instCompleteLattice
The inf is not explicit over there, it is deduced from an sInf construction.

[Rémy Degenne]

We should add all the missing API necessary to make that equivalence easy to prove, and add the proof of the equivalence itself.
Then comes the next question: should we keep the MutuallySingular definition or use Disjoint?

[Kexing Ying]

I think its a good idea to make it a special case once all the equivalences are there.

[Kexing Ying]

Sorry free version:

import Mathlib

namespace MeasureTheory

open ENNReal Set Filter NNReal
open scoped Filter

variable {α} {_ : MeasurableSpace α} {μ ν : Measure α}

lemma Measure.inf_apply {s : Set α} (hs : MeasurableSet s) :
    (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} := by
  rw [← sInf_pair, Measure.sInf_apply hs, OuterMeasure.sInf_apply
    (image_nonempty.2 <| insert_nonempty μ {ν})]
  refine le_antisymm ?_ ?_
  · refine le_sInf fun m ⟨t, ht₁⟩ ↦ ?_
    subst ht₁
    set t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅ with ht'
    refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_
    · by_cases hxt : x ∈ t
      · refine mem_iUnion.2 ⟨0, ?_⟩
        simp [hx, hxt]
      · refine mem_iUnion.2 ⟨1, ?_⟩
        simp [hx, hxt]
    · simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
      rw [tsum_eq_add_tsum_ite 0, tsum_eq_add_tsum_ite 1, if_neg zero_ne_one.symm,
        (tsum_eq_zero_iff ENNReal.summable).2 _, add_zero]
      · exact add_le_add (inf_le_left.trans <| by simp [ht']) (inf_le_right.trans <| by simp [ht'])
      · simp only [ite_eq_then]
        intro n hn₁ hn₀
        simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, iInf_pair, le_refl, inf_of_le_left]
  · refine le_iInf₂ fun t' ht' ↦ ?_
    simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
    set t := ⋃ n ∈ {k : ℕ | μ (t' k) ≤ ν (t' k)}, t' n with ht
    suffices : μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' n, μ (t' n) ⊓ ν (t' n)
    · refine le_trans (sInf_le ⟨t, rfl⟩) this
    have hle₁ : μ (t ∩ s) ≤ ∑' (n : {k | μ (t' k) ≤ ν (t' k)}), μ (t' n) :=
      (measure_mono inter_subset_left).trans <| measure_biUnion_le _ (to_countable _) _
    have hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k : ℕ | ν (t' k) < μ (t' k)}, t' n
    · simp_rw [ht, compl_iUnion]
      refine fun x ⟨hx₁, hx₂⟩ ↦ mem_iUnion₂.2 ?_
      rw [mem_iInter₂] at hx₁
      obtain ⟨i, hi⟩ := mem_iUnion.1 <| ht' hx₂
      refine ⟨i, ?_, hi⟩
      by_contra h
      simp only [mem_setOf_eq, not_lt] at h
      exact hx₁ i h hi
    have hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : {k | ν (t' k) < μ (t' k)}), ν (t' n) :=
      (measure_mono hcap).trans (measure_biUnion_le ν (to_countable {k | ν (t' k) < μ (t' k)}) _)
    refine (add_le_add hle₁ hle₂).trans ?_
    have heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
    · ext k
      simp [le_or_lt]
    conv in ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n) => rw [← tsum_univ, ← heq]
    rw [tsum_union_disjoint (f := fun n ↦ μ (t' n) ⊓ ν (t' n)) ?_ ENNReal.summable ENNReal.summable]
    · refine add_le_add (tsum_congr ?_).le (tsum_congr ?_).le
      · rw [Subtype.forall]
        intro n hn; simpa
      · rw [Subtype.forall]
        intro n hn
        rw [mem_setOf_eq] at hn
        simp [le_of_lt hn]
    · rw [Set.disjoint_iff]
      rintro k ⟨hk₁, hk₂⟩
      rw [mem_setOf_eq] at hk₁ hk₂
      exact False.elim <| hk₂.not_le hk₁

lemma aux₁ {s : Set ℝ≥0∞} (h : s.Nonempty) (hs : sInf s = 0) (n : ℕ) {ε : ℝ≥0} (hε : 0 < ε) :
    ∃ x ∈ s, x < ε * (1 / 2 : ℝ≥0∞) ^ n := by
  refine exists_lt_of_csInf_lt h <| hs ▸ ENNReal.mul_pos ?_ (by simp)
  norm_cast
  exact hε.ne.symm

lemma aux₂ {x : ℝ≥0∞} {ε : ℝ≥0}
    (h : ∀ n : ℕ, x ≤ ε * (1 / 2) ^ n) : x = 0 := by
  rw [← nonpos_iff_eq_zero]
  refine ge_of_tendsto' (f := fun (n : ℕ) ↦ ε * (1 / 2 : ℝ≥0∞) ^ n) (x := atTop) ?_ h
  rw [← mul_zero (M₀ := ℝ≥0∞) (a := ε)]
  exact Tendsto.const_mul (tendsto_pow_atTop_nhds_zero_of_lt_one <| by norm_num) (Or.inr coe_ne_top)

lemma foo : ∑' (n : ℕ), (1 / 2 : ℝ≥0∞) ^ n = 2 := by
  simp only [one_div, tsum_geometric, one_sub_inv_two, inv_inv]

lemma aux₃ {ε : ℝ≥0∞} : ∑' (n : ℕ), ε * (1 / 2) ^ n = 2 * ε := by
  conv in 2 * ε => rw [← foo]
  rw [mul_comm]
  exact ENNReal.tsum_mul_left

lemma Disjoint.mutuallySingular' (h : Disjoint μ ν) (ε : ℝ≥0) (hε : 0 < ε) :
    ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ε := by
  have h₁ : (μ ⊓ ν) univ = 0 := le_bot_iff.1 (h (inf_le_left (b := ν)) inf_le_right) ▸ rfl
  simp_rw [Measure.inf_apply MeasurableSet.univ, inter_univ] at h₁
  have h₂ : ∀ n : ℕ, ∃ t, μ t + ν tᶜ < ε * (1 / 2) ^ n := by
    intro n
    have hn : {m | ∃ t, m = μ t + ν tᶜ}.Nonempty := ⟨ν univ, ∅, by simp⟩
    obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ := aux₁ hn h₁ n hε
    exact ⟨t, hm₂⟩
  choose t ht₂ using h₂
  refine ⟨⋂ n, t n, ?_, ?_⟩
  · refine aux₂ <| fun n ↦ ((measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans
      (le_add_right le_rfl)).trans (ht₂ n).le
  · rw [compl_iInter]
    refine (measure_iUnion_le _).trans (aux₃ ▸ ?_)
    exact tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
      ENNReal.summable ENNReal.summable

lemma Disjoint.mutuallySingular'' (h : Disjoint μ ν) (n : ℕ) :
    ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n := by
  have := Disjoint.mutuallySingular' h ((1 / 2) ^ (n + 1)) <| pow_pos (by simp) (n + 1)
  convert this
  push_cast
  rw [pow_succ, ← mul_assoc, mul_comm, ← mul_assoc]
  norm_cast
  rw [div_mul_cancel₀, one_mul]
  · push_cast
    simp
  · simp

lemma Disjoint.mutuallySingular (h : Disjoint μ ν) : μ ⟂ₘ ν := by
  choose s hs₂ hs₃ using Disjoint.mutuallySingular'' h
  refine Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_
  · rw [compl_iUnion]
    refine aux₂ (ε := 1) <| fun n ↦ ?_
    rw [ENNReal.coe_one, one_mul]
    exact (measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)
  · rw [union_compl_self]

end MeasureTheory

[Rémy Degenne]

@Kexing Ying opened a PR: #17995

[Rémy Degenne]

Disjoint μ ν relates to results about the order on measures like MeasureTheory.Measure.MutuallySingular.mono but it won't help us talk about absolute continuity results like MeasureTheory.Measure.MutuallySingular.mono_ac.

We should also prove an equivalence with Disjoint (ae μ) (ae ν).

[Rémy Degenne]

Here are two implications to prove it (together with the code above):

import Mathlib

namespace MeasureTheory

open ENNReal Set Filter NNReal
open scoped Filter

variable {α} {_ : MeasurableSpace α} {μ ν : Measure α}

lemma Measure.inf_apply {s : Set α} (hs : MeasurableSet s) :
    (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} := sorry

lemma Disjoint.mutuallySingular (h : Disjoint μ ν) : μ ⟂ₘ ν := sorry

lemma MutuallySingular.disjoint_ae (h : μ ⟂ₘ ν) : Disjoint (ae μ) (ae ν) := by
  rw [disjoint_iff_inf_le]
  intro s _
  refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
  · rw [mem_ae_iff, compl_union, compl_compl]
    exact measure_inter_null_of_null_right _ h.measure_nullSet
  · rw [mem_ae_iff, compl_union]
    exact measure_inter_null_of_null_right _ h.measure_compl_nullSet
  · rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl, ← compl_union, compl_compl,
      inter_union_compl, compl_compl]

lemma disjoint_of_disjoint_ae (h : Disjoint (ae μ) (ae ν)) : Disjoint μ ν := by
  rw [disjoint_iff_inf_le] at h ⊢
  refine Measure.le_intro fun s hs _ ↦ ?_
  rw [Measure.inf_apply hs]
  have : (⊥ : Measure α) = 0 := rfl
  simp only [this, Measure.coe_zero, Pi.zero_apply, nonpos_iff_eq_zero]
  specialize h (mem_bot (s := sᶜ))
  rw [mem_inf_iff] at h
  obtain ⟨t₁, ht₁, t₂, ht₂, h_eq'⟩ := h
  have h_eq : s = t₁ᶜ ∪ t₂ᶜ := by
    rw [union_eq_compl_compl_inter_compl, compl_compl, compl_compl, ← h_eq', compl_compl]
  rw [mem_ae_iff] at ht₁ ht₂
  refine le_antisymm ?_ zero_le'
  refine sInf_le_of_le (a := 0) (b := 0) ?_ le_rfl
  rw [h_eq]
  refine ⟨t₁ᶜ ∩ t₂, Eq.symm ?_⟩
  rw [add_eq_zero]
  constructor
  · refine measure_inter_null_of_null_left _ ?_
    exact measure_inter_null_of_null_left _ ht₁
  · rw [compl_inter, compl_compl, union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl, ← compl_union,
      compl_compl, compl_compl, inter_comm, inter_comm t₁, union_comm, inter_union_compl]
    exact ht₂

end MeasureTheory

[Rémy Degenne]

(yes I got lost in the set manipulations at some points. golf welcome :) )

[Rémy Degenne]

In summary: μ ⟂ₘ ν ↔ Disjoint μ ν ↔ Disjoint (ae μ) (ae ν)

[Kexing Ying]

Would you like me to include this in #17995

[Rémy Degenne]

Yes please!