inv_rnDeriv' — Mathlib

English

A variant of inv_rnDeriv asserting the same reciprocal relationship under σ-finiteness and absolute continuity conditions.

Русский

Вариант inv_rnDeriv с тем же отношением обратного отношения при условии σ-конечности и абсолютной непрерывности.

LaTeX

$$$(ν.rnDeriv μ)^{-1} =_{μ}^{ae} μ.rnDeriv ν$$$

Lean4

theorem inv_rnDeriv' [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) : (ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν := by
  filter_upwards [inv_rnDeriv hμν] with x hx; simp only [Pi.inv_apply, ← hx, inv_inv]

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