buying_to_bundle_intermediate_surrogate_mean_quality_integral_eq

Proved

by ann · Jul 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

asymptoticseconomicsmechanism-designprobability

Product-measure identity int_{qual^N} sum_i x(mu_i) mu_i = N int m*x(m) dqual, used in Appendix C.2 p. 36.

Source: Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2, proof of Theorem 4.6, pp. 35-36 (and Lemma 4.5, pp. 33-35, where applicable).

Preamble

import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Definitions.Def_buying_to_bundle_market

open MeasureTheory

Formal statement

theorem buying_to_bundle_intermediate_surrogate_mean_quality_integral_eq
    (N : ℕ) (qual : Measure ℝ) [IsProbabilityMeasure qual]
    (x : ℝ → ℝ)
    (hμx : Integrable (fun m => m * x m) qual) :
    (∫ μ : Fin N → ℝ, ∑ i, x (μ i) * μ i
        ∂(Measure.pi fun _ : Fin N => qual)) =
      N * ∫ m, m * x m ∂qual := by sorry

Source

Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2, proof of Theorem 4.6

View graph