6.1. Almost Everywhere🔗

Let X be a measurable space, and let \mu be a measure on X.

Definition.

Let P(x) be a property of points x \in X. We say that P holds almost everywhere with respect to \mu (or P(x) holds for \mu-a.e. x \in X) if the exceptional set has outer measure zero: \mu^* (\{x \in X \mid \neg P(x)\}) = 0. Here \mu^{*} denotes the outer measure associated with \mu.

Lean code

theorem ae_iff {p : α → Prop} : (∀ᵐ a ∂μ, p a) ↔ μ { a | ¬p a } = 0 :=
  Iff.rfl

Lemma.

Let f, g : X \to [0,\infty]. If f = g almost everywhere, then their lower Lebesgue integrals are equal: \underline{\int}_{x \in X} f(x)\,d\mu = \underline{\int}_{x \in X} g(x)\,d\mu.

Lean code

theorem SimpleFunc.measure_preimage_singleton_congr_ae (f g : SimpleFunc X)
    (hfg : ∀ᵐ x ∂μ, f x = g x) (y : ℝ≥0∞) :
    μ (f ⁻¹' {y}) = μ (g ⁻¹' {y}) := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
  have hnull : μ {x | f x ≠ g x} = 0 := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
    simpa [ae_iff] using hfgAll goals completed! 🐙
  have hfg_diff : μ (f ⁻¹' {y} \ g ⁻¹' {y}) = 0 := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
    refine measure_mono_null (preimage_singleton_diff_subset_setOf_ne f g y) hnullAll goals completed! 🐙
  have hgf_diff : μ (g ⁻¹' {y} \ f ⁻¹' {y}) = 0 := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞⊢ μ (⇑f ⁻¹' {y}) = μ (⇑g ⁻¹' {y})
    refine measure_mono_null (preimage_singleton_diff_subset_setOf_ne g f y) ?_X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:SimpleFunc Xg:SimpleFunc Xhfg:∀ᵐ (x : X) ∂μ, f x = g xy:ℝ≥0∞hnull:μ {x | f x ≠ g x} = 0 := id (Eq.mp measure_preimage_singleton_congr_ae._simp_1 hfg)hfg_diff:μ (⇑f ⁻¹' {y} \ ⇑g ⁻¹' {y}) = 0 := measure_mono_null (preimage_singleton_diff_subset_setOf_ne (⇑f) (⇑g) y) hnull⊢ μ {x | g x ≠ f x} = 0
    simpa [ne_comm] using hnullAll goals completed! 🐙
  exact measure_congr_of_diff_eq_zero
    (f.measurableSet_fiber y) (g.measurableSet_fiber y) hfg_diff hgf_diffAll goals completed! 🐙

theorem lintegral_mono_ae {f g : X → ℝ≥0∞} (hfg : ∀ᵐ x ∂μ, f x ≤ g x) :
    ∫⁻ x, f x ∂μ ≤ ∫⁻ x, g x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
  let ⟨t, hts, ht, ht0⟩ := exists_measurable_superset_of_null hfgX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
  have h_ae_not_mem : ∀ᵐ x ∂μ, x ∉ t := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ simpa [ae_iff] using ht0All goals completed! 🐙
  rw [lintegral, lintegral]X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun x => g x), g_1.lintegral μ
  refine iSup₂_le fun s hsf ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_refine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ ⇑(s.restrict tᶜ) ≤ fun x => g xrefine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ
  ·refine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ ⇑(s.restrict tᶜ) ≤ fun x => g x intro xrefine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:X⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x
    by_cases hx : x ∈ tposX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∈ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) xnegX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∉ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x
    ·posX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∈ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x rw [SimpleFunc.restrict_apply _ ht.compl,
        Set.indicator_of_notMem (show x ∉ tᶜ by simpa using hx)]posX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∈ t⊢ 0 ≤ (fun x => g x) x
      exact bot_leAll goals completed! 🐙
    ·negX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∉ t⊢ (s.restrict tᶜ) x ≤ (fun x => g x) x have hsxg : s x ≤ g x := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
        exact le_trans (hsf x) (by_contra fun hxfg ↦ hx (hts hxfg))All goals completed! 🐙
      rw [SimpleFunc.restrict_apply _ ht.compl, indicator_of_mem hx]negX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhx:x ∉ thsxg:s x ≤ g x := le_trans (hsf x) (by_contra fun hxfg => hx (hts hxfg))⊢ s x ≤ (fun x => g x) x
      exact hsxgAll goals completed! 🐙
  ·refine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f x⊢ s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ have h_restrict : ∀ᵐ x ∂μ, s x = s.restrict tᶜ x := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ
      exact h_ae_not_mem.mono fun x hxt ↦ byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x ≤ g xt:Set Xhts:{x | (fun x => f x ≤ g x) x}ᶜ ⊆ tht:MeasurableSet tht0:μ t = 0h_ae_not_mem:∀ᵐ (x : X) ∂μ, x ∉ t := 
  Eq.mpr
    (id
      (Eq.trans SimpleFunc.measure_preimage_singleton_congr_ae._simp_1
        (congrFun' (congrArg Eq (congrArg (⇑μ) (congrArg setOf (funext fun a => Classical.not_not._simp_1)))) 0)))
    ht0s:SimpleFunc Xhsf:⇑s ≤ fun x => f xx:Xhxt:x ∉ t⊢ s x = (s.restrict tᶜ) x
        rw [SimpleFunc.restrict_apply _ ht.compl, indicator_of_mem hxt]All goals completed! 🐙
    exact le_of_eq <| SimpleFunc.lintegral_eq_of_measure_preimage
      (SimpleFunc.measure_preimage_singleton_congr_ae (μ := μ) s (s.restrict tᶜ) h_restrict)All goals completed! 🐙

theorem lintegral_congr_ae {f g : X → ℝ≥0∞} (hfg : ∀ᵐ x ∂μ, f x = g x) :
    ∫⁻ x, f x ∂μ = ∫⁻ x, g x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), f x ∂μ = ∫⁻ (x : X), g x ∂μ
  apply le_antisymmaX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μaX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), g x ∂μ ≤ ∫⁻ (x : X), f x ∂μ
  ·aX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), f x ∂μ ≤ ∫⁻ (x : X), g x ∂μ exact lintegral_mono_ae <| hfg.mono fun x hx ↦ hx.leAll goals completed! 🐙
  ·aX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hfg:∀ᵐ (x : X) ∂μ, f x = g x⊢ ∫⁻ (x : X), g x ∂μ ≤ ∫⁻ (x : X), f x ∂μ exact lintegral_mono_ae <| hfg.mono fun x hx ↦ hx.geAll goals completed! 🐙