Product-measure helpers

Small pieces of product-measure theory with no L² or inner-product content.

• TauCeti.ae_of_ae_fst / TauCeti.ae_of_ae_snd transfer an a.e. statement about one factor to the product measure, along Measure.quasiMeasurePreserving_fst / _snd.
• TauCeti.measurable_setLIntegral_of_measurableSet proves measurability of a set integral whose truncating relation is jointly measurable.
• TauCeti.lintegral_mul_setLIntegral_eq exchanges a weighted integral of set integrals over an arbitrary parameter measure with the corresponding integral over the sections of the truncating relation.
• TauCeti.lintegral_cond_prod_le bounds a lower Lebesgue integral over a product of two conditional laws by any bound the integrand satisfies on the rectangle conditioned on. Use it to estimate an integral against two independently conditioned coordinates when the integrand is controlled only on the pair of sets being conditioned on.
• TauCeti.setIntegral_eq_zero_of_forall_prod is the binary-product specialization of the Dynkin (π-λ) step for Bochner integrals: a function whose integral vanishes on every measurable rectangle has vanishing integral on every measurable set. Rectangles are a π-system generating the product σ-algebra (MeasureTheory.isPiSystem_prod, MeasureTheory.generateFrom_prod), so this is the general TauCeti.setIntegral_eq_zero_of_isPiSystem instantiated at that π-system; the only work left here is extracting the whole-space hypothesis from the rectangle univ ×ˢ univ.

theorem TauCeti.measurable_setLIntegral_of_measurableSet {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {g : α → ENNReal} {R : γ → α → Prop} (hR : MeasurableSet {z : γ × α | R z.1 z.2}) (hg : AEMeasurable g μ) : Measurable fun (t : γ) => ∫⁻ (x : α) in {x : α | R t x}, g x ∂μ

The truncated integral t ↦ ∫⁻ x in {x | R t x}, g x ∂μ of an a.e.-measurable integrand is measurable when the truncating relation is jointly measurable.

theorem TauCeti.lintegral_mul_setLIntegral_eq {α : Type u_1} {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : MeasureTheory.Measure γ} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite κ] {g : α → ENNReal} {w : γ → ENNReal} {R : γ → α → Prop} (hR : MeasurableSet {z : γ × α | R z.1 z.2}) (hg : AEMeasurable g μ) (hw : AEMeasurable w κ) : ∫⁻ (t : γ), w t * ∫⁻ (x : α) in {x : α | R t x}, g x ∂μ ∂κ = ∫⁻ (x : α), (∫⁻ (t : γ), {t : γ | R t x}.indicator w t ∂κ) * g x ∂μ

Tonelli for a weighted integral of truncated integrals. For a jointly measurable truncating relation R and a.e.-measurable integrand and weight, integrating first in x and then against the parameter measure gives the same value as integrating the weight over each parameter section and then in x.

theorem TauCeti.ae_of_ae_fst {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {p : α → Prop} (hp : ∀ᵐ (x : α) ∂μ, p x) : ∀ᵐ (q : α × β) ∂μ.prod ν, p q.1

An a.e. statement on the first factor transfers to the product measure.

theorem TauCeti.ae_of_ae_snd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {p : β → Prop} (hp : ∀ᵐ (y : β) ∂ν, p y) : ∀ᵐ (q : α × β) ∂μ.prod ν, p q.2

An a.e. statement on the second factor transfers to the product measure.

theorem TauCeti.lintegral_cond_prod_le {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) (hμ : μ s ≠ 0) (hμtop : μ s ≠ ⊤) (hν : ν t ≠ 0) (hνtop : ν t ≠ ⊤) {f : α × β → ENNReal} {b : ENNReal} (hf : ∀ x ∈ s, ∀ y ∈ t, f (x, y) ≤ b) : ∫⁻ (z : α × β), f z ∂μ[|s].prod ν[|t] ≤ b

A rectangle bound for an integral against a product of conditional laws. If f is bounded by b on s ×ˢ t, then its lower Lebesgue integral against the product of the laws of μ and ν conditioned on s and on t is at most b: conditioning confines each coordinate to its own set almost surely, so the bound holds almost everywhere on the product.

theorem TauCeti.setIntegral_eq_zero_of_forall_prod {α : Type u_1} {β : Type u_2} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : MeasureTheory.Measure (α × β)} {f : α × β → E} (hf : MeasureTheory.Integrable f ρ) (hrect : ∀ (s : Set α), MeasurableSet s → ∀ (t : Set β), MeasurableSet t → ∫ (p : α × β) in s ×ˢ t, f p ∂ρ = 0) (u : Set (α × β)) : MeasurableSet u → ∫ (p : α × β) in u, f p ∂ρ = 0

The Dynkin (π-λ) step for Bochner integrals on a product space. A function whose integral vanishes on every measurable rectangle has vanishing integral on every measurable set.

This is TauCeti.setIntegral_eq_zero_of_isPiSystem at the π-system of measurable rectangles.