rnDeriv_pos — Mathlib

English

If κ a ≪ η a, then rnDeriv κ η a x > 0 on a set of positive η a-measure; equivalently, 0 < rnDeriv κ η a x almost everywhere on the support where absolute continuity holds.

Русский

Если κ a эквивалентно η a (κ a ≪ η a), то rnDeriv κ η a x > 0 на множестве с позитивной η a-массой; фактически, почти всюду на поддержке, где выполняется абсолютная непрерывность, плотность положительна.

LaTeX

$$ha := κ a ≪ η a → ∀ᵐ x ∂(η a), 0 < rnDeriv κ η a x$$

Lean4

theorem rnDeriv_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (ha : κ a ≪ η a) : ∀ᵐ x ∂(κ a), 0 < rnDeriv κ η a x :=
  by filter_upwards [ha.ae_le κ.rnDeriv_eq_rnDeriv_measure, Measure.rnDeriv_pos ha] with x heq hpos using heq ▸ hpos

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