absolutelyContinuous_withDensity_rnDeriv

English

If [HaveLebesgueDecomposition ν μ] and μ ≪ ν, then μ ≪ μ.withDensity(ν.rnDer μ).

Русский

Пусть [HaveLebesgueDecomposition ν μ] и μ ≪ ν; тогда μ ≪ μ.withDensity(ν.rnDer μ).

LaTeX

$$$$ [HaveLebesgueDecomposition\ ν\ μ] \; (μ \ll ν) \Rightarrow μ \ll μ.withDensity(ν.rnDer μ) $$$$

Lean4

theorem absolutelyContinuous_withDensity_rnDeriv [HaveLebesgueDecomposition ν μ] (hμν : μ ≪ ν) :
    μ ≪ μ.withDensity (ν.rnDeriv μ) :=
  by
  rw [haveLebesgueDecomposition_add ν μ] at hμν
  refine AbsolutelyContinuous.mk (fun s _ hνs ↦ ?_)
  obtain ⟨t, _, ht1, ht2⟩ := mutuallySingular_singularPart ν μ
  rw [← inter_union_compl s]
  refine le_antisymm ((measure_union_le (s ∩ t) (s ∩ tᶜ)).trans ?_) (zero_le _)
  simp only [nonpos_iff_eq_zero, add_eq_zero]
  constructor
  · refine hμν ?_
    simp only [coe_add, Pi.add_apply, add_eq_zero]
    constructor
    · exact measure_mono_null Set.inter_subset_right ht1
    · exact measure_mono_null Set.inter_subset_left hνs
  · exact measure_mono_null Set.inter_subset_right ht2

Похожие утверждения