rnDeriv_def — Mathlib

English

The Radon-Nikodym derivative rnDeriv κ η equals ENNReal.ofReal(rnDerivAux κ (κ+η) a x) divided by ENNReal.ofReal(1 − rnDerivAux κ (κ+η) a x).

Русский

Плотность rnDeriv κ η равна ENNReal.ofReal(rnDerivAux κ (κ+η) a x) делить на ENNReal.ofReal(1 − rnDerivAux κ (κ+η) a x).

LaTeX

$$$ rnDeriv\ (\kappa\,\eta)\ a\ x = \dfrac{\mathrm{ENNReal}.ofReal( rnDerivAux(\kappa, (\kappa+\eta)) (a, x) )}{\mathrm{ENNReal}.ofReal\left(1 - rnDerivAux(\kappa, (\kappa+\eta)) (a, x)\right)} $$$

Lean4

theorem rnDeriv_def : eta_helper Eq✝ @rnDeriv.{} @(delta% @definition✝) :=
  by
  intros
  delta rnDeriv
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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