L¹ convergence of a finite product

If finitely many families of unit-ball-valued functions each converge in L¹, then their pointwise product converges in L¹ to the product of the limits:

∫ ‖∏ i ∈ s, F i j ω - ∏ i ∈ s, g i ω‖ ∂μ → 0.

The whole content is the pointwise telescoping bound norm_prod_sub_prod_le_sum_norm_sub, which turns the integrand into a finite sum of the individual discrepancies; integrating and summing then gives the result with no Hölder or dominated-convergence machinery.

The unit-ball hypotheses are what make the constant 1: for indicator observables both a block average and its conditional expectation lie in [0, 1], which is the motivating case. That motivation is TauCetiRoadmap/Exchangeability/README.md, Layer 3 (the L² averaging library and the standard-Borel de Finetti route): this is the step from "each window average converges in L¹" to "the product of finitely many window averages converges in L¹", which the disjoint-window block factorization consumes. Layer 5's Koopman route needs the same step against a different conditioning σ-algebra, which is why this is neutral infrastructure rather than living inside either route.

Everything is stated for an arbitrary Finset ι of factors, an arbitrary filter on the approximating index, and an arbitrary seminormed commutative ring of values, with a.e. bounds and AEStronglyMeasurable hypotheses, since that is all the integral sees. Nothing here mentions a process, a σ-algebra or exchangeability.

theorem TauCeti.MeasureTheory.tendsto_integral_norm_prod_sub_prod {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {ι' : Type u_3} {R : Type u_4} [SeminormedCommRing R] [NormOneClass R] {l : Filter ι'} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Finset ι} {F : ι → ι' → Ω → R} {g : ι → Ω → R} (hF_meas : ∀ i ∈ s, ∀ (j : ι'), MeasureTheory.AEStronglyMeasurable (F i j) μ) (hg_meas : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (g i) μ) (hF_le : ∀ i ∈ s, ∀ (j : ι'), ∀ᵐ (ω : Ω) ∂μ, ‖F i j ω‖ ≤ 1) (hg_le : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, ‖g i ω‖ ≤ 1) (hconv : ∀ i ∈ s, Filter.Tendsto (fun (j : ι') => ∫ (ω : Ω), ‖F i j ω - g i ω‖ ∂μ) l (nhds 0)) : Filter.Tendsto (fun (j : ι') => ∫ (ω : Ω), ‖∏ i ∈ s, F i j ω - ∏ i ∈ s, g i ω‖ ∂μ) l (nhds 0)

A finite product of unit-ball families converges in L¹. If each of finitely many families F i · converges to g i in L¹, and every value lies almost everywhere in the closed unit ball, then the product ∏ i ∈ s, F i j converges to ∏ i ∈ s, g i in L¹.