rnDeriv_eq_one_iff_eq — Mathlib

English

If κ a ≪ η a, then the RN-derivative κ.rnDeriv η a equals 1 almost everywhere with respect to η a if and only if κ a = η a.

Русский

Если κ a ≪ η a, то rnDeriv η a равна единице почти по η a тогда и только тогда κ a = η a.

LaTeX

$$[$ (∀ᵐ b ∂(η a), κ.rnDeriv η a b = 1) \\iff κ a = η a $]$$

Lean4

theorem rnDeriv_eq_one_iff_eq [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h_ac : κ a ≪ η a) :
    (∀ᵐ b ∂(η a), κ.rnDeriv η a b = 1) ↔ κ a = η a :=
  by
  rw [← Measure.rnDeriv_eq_one_iff_eq h_ac]
  refine eventually_congr ?_
  filter_upwards [rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with c hc
  rw [hc, Pi.one_apply]

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