Lebesgue integral utilities

This file provides helper lemmas for the Lebesgue integral with Dirac measures.

Main declarations

• lintegral_lintegral_dirac: computing nested integrals with Dirac measures.

theorem lintegral_lintegral_dirac {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : β → ENNReal} {g : α → β} (hf : Measurable f) : ∫⁻ (a : α), ∫⁻ (b : β), f b ∂MeasureTheory.Measure.dirac (g a) ∂μ = ∫⁻ (a : α), f (g a) ∂μ