rnDeriv — Mathlib

English

The Radon–Nikodym derivative of a complex measure with respect to a measure is integrable with respect to that measure.

Русский

Производная Радона–Никодымова для комплексной меры по отношению к мере интегрируема по этой мере.

LaTeX

$$$ Integrable (c.rnDeriv \\mu) \\mu $$$

Lean4

/-- The Radon-Nikodym derivative between a complex measure and a positive measure. -/
def rnDeriv (c : ComplexMeasure α) (μ : Measure α) : α → ℂ := fun x => ⟨c.re.rnDeriv μ x, c.im.rnDeriv μ x⟩

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