Representatives and integration under measure completion #
Events in a sigma-algebra augmented by null sets have almost-everywhere representatives in the original sigma-algebra. Integration of a real function against the completed measure agrees with integration against the original measure, globally and on measurable sets.
theorem
BGW.Probability.exists_raw_ae_eq_of_mem_sup
{Ω : Type u_1}
[MeasurableSpace Ω]
(P : MeasureTheory.Measure Ω)
{m : MeasurableSpace Ω}
{A : Set Ω}
(hA : MeasurableSet A)
:
∃ (B : Set Ω), MeasurableSet B ∧ A =ᵐ[P] B
An event in the join of a sigma-algebra with the null-set sigma-algebra has a representative in the original sigma-algebra, almost everywhere equal to the given event.
theorem
BGW.Probability.integral_completion
{Ω : Type u_1}
[MeasurableSpace Ω]
(P : MeasureTheory.Measure Ω)
{F : Ω → ℝ}
(hF : MeasureTheory.AEStronglyMeasurable F P)
:
Real integration against a completed measure equals integration against the original measure.
theorem
BGW.Probability.setIntegral_completion
{Ω : Type u_1}
[MeasurableSpace Ω]
(P : MeasureTheory.Measure Ω)
{A : Set Ω}
(hA : MeasurableSet A)
{F : Ω → ℝ}
(hF : MeasureTheory.AEStronglyMeasurable F P)
:
Set integration against a completed measure equals set integration against the original measure on every measurable set.