rnDeriv_def — Mathlib

English

The function rnDeriv s μ is defined by rnDeriv s μ x = (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal − (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal.

Русский

Функция rnDeriv s μ определяется как rnDeriv s μ x = (s^{+}_{μ}.rnDeriv μ x)^{Real} − (s^{-}_{μ}.rnDeriv μ x)^{Real}.

LaTeX

$$rnDeriv (s) (μ) = fun x => (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal$$

Lean4

theorem rnDeriv_def (s : SignedMeasure α) (μ : Measure α) :
    rnDeriv s μ = fun x =>
      (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal :=
  rfl

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