Theorems · Inductive type · measure theory

MeasureTheory.Measure.HaveLebesgueDecomposition

{α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Prop

A pair of measures μ and ν is said to HaveLebesgueDecomposition if there exists a measure ξ and a measurable function f, such that ξ is mutually singular with respect to ν and μ = ξ + ν.withDensity f.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Cited by

92 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms