A Dynkin (π-λ) step for Bochner integrals #
If a function's integral vanishes on the whole space and on every member of a π-system generating the σ-algebra, then it vanishes on every measurable set.
This is the Bochner counterpart of Mathlib's ℝ≥0∞-valued
MeasureTheory.lintegral_eq_lintegral_of_isPiSystem. Stating it for an arbitrary π-system rather
than for a specific one (rectangles, boxes) lets a single theorem serve every product-measure
arity.
theorem
TauCeti.setIntegral_eq_zero_of_isPiSystem
{X : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace X}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{ρ : MeasureTheory.Measure X}
{S : Set (Set X)}
(hgen : m0 = MeasurableSpace.generateFrom S)
(hpi : IsPiSystem S)
{f : X → E}
(hf : MeasureTheory.Integrable f ρ)
(huniv : ∫ (x : X), f x ∂ρ = 0)
(hS : ∀ s ∈ S, ∫ (x : X) in s, f x ∂ρ = 0)
(u : Set X)
:
The Dynkin (π-λ) step for Bochner integrals. A function whose integral vanishes on the whole space and on every member of a generating π-system has vanishing integral on every measurable set.