withDensity_absolutelyContinuous — Mathlib

English

For any a, the density η.withDensity (κ.rnDeriv η) a is absolutely continuous with respect to κ a.

Русский

Для любого a мера η.withDensity (κ.rnDeriv η) a абсолютно непряма по отношению к κ a.

LaTeX

$$η.withDensity (κ.rnDeriv η) a ≪ κ a$$

Lean4

nonrec theorem withDensity_absolutelyContinuous [IsSFiniteKernel κ] (f : α → β → ℝ≥0∞) (a : α) :
    Kernel.withDensity κ f a ≪ κ a :=
  by
  by_cases hf : Measurable (Function.uncurry f)
  · rw [Kernel.withDensity_apply _ hf]
    exact withDensity_absolutelyContinuous _ _
  · rw [withDensity_of_not_measurable _ hf]
    simp [Measure.AbsolutelyContinuous.zero]

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