AutoSamplingTheory.TechnicalLemmas.Analysis.DiagonalProductCostIntegral

- Under a finite product of probability laws on pairs, the expected diagonal quadratic cost is the sum of the expected one-coordinate quadratic costs.

theorem integral_diagonalQuadraticCost_eq_sum
    (mu : I → ProbabilityMeasure (E × E))
    (hcost : ∀ i, Integrable (fun z : E × E => ‖z.1 - z.2‖ ^ 2)
      (mu i : Measure (E × E))) :
    (∫ q : I → E × E, diagonalQuadraticCost q
        ∂Measure.pi (fun i => (mu i : Measure (E × E)))) =
      ∑ i, ∫ z : E × E, ‖z.1 - z.2‖ ^ 2 ∂(mu i : Measure (E × E)) := by
  classical
  rw [diagonalQuadraticCost]
  rw [integral_finset_sum]
  · apply Finset.sum_congr rfl
    intro i _hi
    exact integral_comp_eval (hcost i).aestronglyMeasurable
  · intro i _hi
    exact integrable_comp_eval (hcost i)

end

end DiagonalProductCostIntegral
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/DiagonalProductCostIntegral.lean:29published source at 0e31a3cda412