withDensity_apply_eq_zero'

Stream: mathlib4

[Gaëtan Serré]

Hello, I was able to relax the measurable hypothesis on withDensity_apply_eq_zero. It gives

theorem withDensity_apply_eq_zero' {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f μ) :
    μ.withDensity f s = 0 ↔ μ ({ x | f x ≠ 0 } ∩ s) = 0 := by
  constructor
  · intro hs
    let t := toMeasurable (μ.withDensity f) s
    apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))
    have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
    rw [withDensity_apply f (measurableSet_toMeasurable _ s), lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
      EventuallyEq, ae_restrict_iff'₀, ae_iff] at A
    swap
    · simp only [measurableSet_toMeasurable, MeasurableSet.nullMeasurableSet]
    simp only [Pi.zero_apply, mem_setOf_eq, Filter.mem_mk] at A
    convert A using 2
    ext x
    simp only [and_comm, exists_prop, mem_inter_iff, iff_self_iff, mem_setOf_eq, mem_compl_iff,
      not_forall]
  · intro hs
    let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)
    have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_setOf_eq, eq_self_iff_true, or_true_iff]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩
    apply measure_mono_null A (measure_union_null _ _)
    · apply withDensity_absolutelyContinuous
      rwa [measure_toMeasurable]
    rcases hf with ⟨g, hg, hfg⟩
    have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} := by
      apply withDensity_absolutelyContinuous
      filter_upwards [hfg] with a ha
      simp only [eq_iff_iff]
      exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
    rw [measure_congr t, withDensity_congr_ae hfg]
    have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)
    rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]
    filter_upwards [ae_restrict_mem M]
    simp only [imp_self, Pi.zero_apply, imp_true_iff]

Then, the proof of withDensity_apply_eq_zero is way simpler:

theorem withDensity_apply_eq_zero {f : α → ℝ≥0∞} {s : Set α} (hf : Measurable f) :
    μ.withDensity f s = 0 ↔ μ ({ x | f x ≠ 0 } ∩ s) = 0 :=
  withDensity_apply_eq_zero' <| Measurable.aemeasurable hf

I will probably be able to prove ae_withDensity_iff and others for AEMeasurable densities but I was wondering if it is desirable to have that in Mathlib.

[Rémy Degenne]

We probably want that lemma in Mathlib. However, the proof can be made much shorter by using that an a.e.-measurable function is almost everywhere equal to a measurable function (for which we can apply the lemma that is already in Mathlib):

import Mathlib.MeasureTheory.Measure.WithDensity

open MeasureTheory Filter
open scoped ENNReal

theorem withDensity_apply_eq_zero' {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f μ) :
    μ.withDensity f s = 0 ↔ μ ({ x | f x ≠ 0 } ∩ s) = 0 := by
  rw [withDensity_congr_ae hf.ae_eq_mk, withDensity_apply_eq_zero hf.measurable_mk]
  suffices {x | AEMeasurable.mk f hf x ≠ 0} =ᵐ[μ] {x | f x ≠ 0} by
    rw [measure_congr (ae_eq_set_inter this EventuallyEq.rfl)]
  filter_upwards [hf.ae_eq_mk] with x hx
  rw [eq_iff_iff]
  change hf.mk f x ≠ 0 ↔ f x ≠ 0
  rw [hx]

Another remark: you code was missing imports. It's much better to write code in this zulip as a #mwe. That way, people can open the online editor with one click and play with your code right away.

[Gaëtan Serré]

Thank you for the advice, I was just trying to naively adapt the original proof. However, in your version, you use withDensity_apply_eq_zero. In my proposition, I prove the latter using withDensity_apply_eq_zero'. I think, at the end, it is shorter as the proof of withDensity_apply_eq_zerois just one line.

[Gaëtan Serré]

import Mathlib

open MeasureTheory Filter Set
open scoped ENNReal

variable [MeasurableSpace α] {μ : Measure α}

theorem withDensity_apply_eq_zero' {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f μ) :
    μ.withDensity f s = 0 ↔ μ ({ x | f x ≠ 0 } ∩ s) = 0 := by
  constructor
  · intro hs
    let t := toMeasurable (μ.withDensity f) s
    apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))
    have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
    rw [withDensity_apply f (measurableSet_toMeasurable _ s), lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
      EventuallyEq, ae_restrict_iff'₀, ae_iff] at A
    swap
    · simp only [measurableSet_toMeasurable, MeasurableSet.nullMeasurableSet]
    simp only [Pi.zero_apply, mem_setOf_eq, Filter.mem_mk] at A
    convert A using 2
    ext x
    simp only [and_comm, exists_prop, mem_inter_iff, iff_self_iff, mem_setOf_eq, mem_compl_iff,
      not_forall]
  · intro hs
    let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)
    have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_setOf_eq, eq_self_iff_true, or_true_iff]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩
    apply measure_mono_null A (measure_union_null _ _)
    · apply withDensity_absolutelyContinuous
      rwa [measure_toMeasurable]
    rcases hf with ⟨g, hg, hfg⟩
    have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} := by
      apply withDensity_absolutelyContinuous
      filter_upwards [hfg] with a ha
      simp only [eq_iff_iff]
      exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
    rw [measure_congr t, withDensity_congr_ae hfg]
    have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)
    rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]
    filter_upwards [ae_restrict_mem M]
    simp only [imp_self, Pi.zero_apply, imp_true_iff]

theorem withDensity_apply_eq_zero {f : α → ℝ≥0∞} {s : Set α} (hf : Measurable f) :
    μ.withDensity f s = 0 ↔ μ ({ x | f x ≠ 0 } ∩ s) = 0 :=
  withDensity_apply_eq_zero' <| Measurable.aemeasurable hf

[Gaëtan Serré]

I guess is more natural to prove withDensity_apply_eq_zero using withDensity_apply_eq_zero' as it is just a specialization of a more general results than the other way around.

[Rémy Degenne]

A counter argument to that could be that your proof for a.e.-measurable uses a reduction to the measurable case in the last part of the proof, and it might be cleaner to do the whole proof for measurable, then extend to a.e.-measurable. :shrug:

I don't really have a strong opinion on that and you can do it as you prefer. Both options are equally good to me, especially since we are discussing two very small lemmas.
I often choose the solution that minimizes the new work to be done: since the other lemma is already there, I would use it.

[Gaëtan Serré]

Good point! I'll see then! Thanks!