Integrating finite products of ℝ≥0∞-valued functions

Two facts about a finite product ∏ i, f i ω of ℝ≥0∞-valued functions, relating its real form to its ℝ≥0∞ form.

Main results

• integrable_prod_toReal — a finite product of measurable [0,1]-valued functions is integrable against a finite measure, since the product is itself [0,1]-valued.
• ofReal_integral_prod_toReal_eq_lintegral_prod — the real integral of the product of the real forms is the lower integral of the product, provided the product is a.e. finite.

Both are stated for an arbitrary family f : ι → Ω → ℝ≥0∞ indexed over a Finset, with almost-everywhere hypotheses, since that is all integration sees. The motivating instance is a product of measure evaluations f i ω = κ ω (B i) for a measurable family of probability measures κ, where the [0,1] bound is prob_le_one and finiteness is measure_ne_top; nothing in the proofs uses that the factors come from measures, so neither statement mentions one.

theorem TauCeti.MeasureTheory.integrable_prod_toReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_2} {ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure ν] {s : Finset ι} {f : ι → Ω → ENNReal} (hf_meas : ∀ i ∈ s, AEMeasurable (f i) ν) (hf_le : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂ν, f i ω ≤ 1) : MeasureTheory.Integrable (fun (ω : Ω) => ∏ i ∈ s, (f i ω).toReal) ν

A finite product of [0,1]-valued functions is integrable against a finite measure: the product is a.e. nonnegative and a.e. bounded by 1, so it is dominated by a constant.

theorem TauCeti.MeasureTheory.ofReal_integral_prod_toReal_eq_lintegral_prod {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_2} {ν : MeasureTheory.Measure Ω} {s : Finset ι} {f : ι → Ω → ENNReal} (hf_ne_top : ∀ᵐ (ω : Ω) ∂ν, ∏ i ∈ s, f i ω ≠ ⊤) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => ∏ i ∈ s, (f i ω).toReal) ν) : ENNReal.ofReal (∫ (ω : Ω), ∏ i ∈ s, (f i ω).toReal ∂ν) = ∫⁻ (ω : Ω), ∏ i ∈ s, f i ω ∂ν

The real integral of a finite product is its ℝ≥0∞ integral. Only the product need be a.e. finite — an infinite factor annihilated by a zero one is fine — since ENNReal.toReal is multiplicative and ENNReal.ofReal_toReal is then applied to the product as a whole.