Theorems · Definition · measure theory

MeasureTheory.Measure.withDensity

{α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → MeasureTheory.Measure α

Given a measure μ : Measure α and a function f : α → ℝ≥0∞, μ.withDensity f is the measure such that for a measurable set s we have μ.withDensity f s = ∫⁻ a in s, f a ∂μ.

Defined in

Mathlib.MeasureTheory.Measure.WithDensity

Cited by

265 results in Mathlib

Foundations

Depth 202 from the axioms, rests on 4,858 definitions · uses propext, Classical.choice, Quot.sound