Product of sums = sum over Pi type?

Stream: Is there code for X?

[David Loeffler]

Mathlib knows that if α and β are Fintypes, and f : α → R and g : β → R are maps into a commutative ring, then (∑ a : α, f a) * (∑ b : β, g b) can be written as a sum over α × β.

Do we have a generalisation of this to a collection of Fintypes indexed by another Fintype, something like
∏ i : d, ∑ x, (f i) x = ∑ z : (i : d) → α i, ∏ i : d, (f i) (z i)?
Mathematically this is "obvious" by induction on the cardinality of the index set, but I can't find a nice way of coding up "induction on the cardinality of a Fintype" in lean.

[Joël Riou]

You may try docs#Finite.induction_empty_option.

[Yaël Dillies]

docs#Finset.prod_sum

[Yaël Dillies]

If you want to avoid dependent type hell: docs#Finset.prod_univ_sum

[David Loeffler]

Great! I will now have a go at proving the analogue for products of integrals (d-dimensional case of Fubini's theorem where d is a Fintype). I'm pretty sure that isn't in the library but I can hopefully use the proof of Finset.prod_univ_sum as a model.

[Floris van Doorn]

I expect formalizing this will be greatly simplified when using docs#MeasureTheory.lmarginal. A version of that using the Bochner integral (which presumably you want?) is forthcoming.

[Floris van Doorn]

Here is a proof using marginals for the Lebesgue integral

import Mathlib.MeasureTheory.Integral.Marginal

open MeasureTheory Classical BigOperators Finset ENNReal

variable {δ : Type*} {π : δ → Type*} [∀ x, MeasurableSpace (π x)]
variable {μ : ∀ i, Measure (π i)} [∀ i, SigmaFinite (μ i)] [DecidableEq δ]
variable {s t : Finset δ} {f g : (∀ i, π i) → ℝ≥0∞} {x y : ∀ i, π i} {i : δ}

variable {α β} [MeasurableSpace α] [MeasurableSpace β] [CommMonoid β] [MeasurableMul₂ β]
theorem Measurable.finset_prod {s : Finset δ} {f : δ → α → β}
    (hf : ∀ i ∈ s, Measurable (f i)) : Measurable fun x ↦ ∏ i in s, f i x := by
  induction s using Finset.induction
  case empty => simp
  case insert i s hi ih =>
    simp_rw [Finset.prod_insert hi]
    exact (hf i (mem_insert_self i s)).mul (ih fun j hj ↦ hf j (mem_insert_of_mem hj))

theorem lmarginal_mul_left {f : (∀ i, π i) → ℝ≥0∞} (hf : Measurable f) (c : ℝ≥0∞) (z : ∀ i, π i) :
    c * (∫⋯∫⁻_s, f ∂μ) z = (∫⋯∫⁻_s, fun x ↦ c * f x ∂μ) z := by
  simp [lmarginal]
  rw [lintegral_const_mul]
  exact hf.comp measurable_updateFinset

theorem lmarginal_smul_left {f : (∀ i, π i) → ℝ≥0∞} (hf : Measurable f) (c : ℝ≥0∞) :
    ∫⋯∫⁻_s, c • f ∂μ = c • ∫⋯∫⁻_s, f ∂μ := by
  ext z
  symm
  apply lmarginal_mul_left hf

theorem lmarginal_prod {s : Finset δ} {f : ∀ i, π i → ℝ≥0∞}
    (hf : ∀ i ∈ s, Measurable (f i)) (z : ∀ i, π i) :
    (∫⋯∫⁻_s, fun x ↦ ∏ i in s, f i (x i) ∂μ) z = ∏ i in s, ∫⁻ x, f i x ∂(μ i) := by
  induction s using Finset.induction
  case empty => simp
  case insert i s hi ih =>
    rw [lmarginal_insert' _ _ hi]
    simp_rw [Finset.prod_insert hi]
    have : ∀ j ∈ s, j ≠ i := by rintro _ _ rfl; contradiction
    simp (config := {contextual := true}) [*]
    simp_rw [lintegral_mul_const _ (hf i (mem_insert_self i s))]
    rw [← lmarginal_mul_left, ih fun j hj ↦ hf j (mem_insert_of_mem hj)]
    exact Measurable.finset_prod fun j hj ↦
      hf j (mem_insert_of_mem hj) |>.comp <| measurable_pi_apply _
    exact Measurable.finset_prod fun j hj ↦
      hf j hj |>.comp <| measurable_pi_apply _

theorem lintegral_finset_prod [Fintype δ] {f : ∀ i, π i → ℝ≥0∞}
    (hf : ∀ i, Measurable (f i)) :
    ∫⁻ x, ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫⁻ x, f i x ∂(μ i) := by
  rcases isEmpty_or_nonempty (∀ i, π i) with h|⟨⟨x⟩⟩
  · simp_rw [lintegral_of_isEmpty]
    simp only [isEmpty_pi] at h
    obtain ⟨i, hi⟩ := h
    rw [prod_eq_zero]
    apply Finset.mem_univ
    exact lintegral_of_isEmpty _ (f i)
  rw [lintegral_eq_lmarginal_univ x, lmarginal_prod (fun i _ ↦ hf i) x]

[David Loeffler]

I was wrong in thinking the version for integrals wasn't in the library – I was searching for by name based on the wrong side of the equation! The result is docs#MeasureTheory.integral_fintype_prod_eq_prod (added in PR #8030 by @Xavier Roblot a few days before my question).

I apologise to @Floris van Doorn – I should have posted in this thread to say that the question was answered.