rnDeriv_def' — Mathlib

English

A variant expression for rnDeriv κ η using rnDerivAux κ (κ+η).

Русский

Вариант выражения rnDeriv κ η через rnDerivAux κ (κ+η).

LaTeX

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

Lean4

theorem rnDeriv_def' (κ η : Kernel α γ) :
    rnDeriv κ η = fun a x ↦ ENNReal.ofReal (rnDerivAux κ (κ + η) a x) / ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a x) :=
  by ext; rw [rnDeriv_def]

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