buying_to_bundle_intermediate_surrogate_payment_cancellation

Proved

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

asymptoticseconomicsmechanism-designprobability

Formal payment-term cancellation in the second-gap proof: expanding surrogatePerSeller turns varpi prime - varpi into revenue minus deterministic mean quality, assuming the two needed integrability hypotheses.

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.Integral.Bochner.Basic
import Definitions.Def_buying_to_bundle_market

open MeasureTheory

Formal statement

theorem buying_to_bundle_intermediate_surrogate_payment_cancellation
    (qual noise : Measure ℝ) (σ : ℝ) (qualPdf : ℝ → ℝ)
    (N : ℕ) (x : ℝ → ℝ) (R : ℝ)
    (hμx : Integrable (fun m => m * x m) qual)
    (hφx : Integrable
      (fun m => BuyingToBundle.virtualCost qual noise σ qualPdf m * x m) qual) :
    ((R -
        N * ∫ m, BuyingToBundle.virtualCost qual noise σ qualPdf m * x m ∂qual) -
      N * BuyingToBundle.surrogatePerSeller qual noise σ qualPdf x) =
      R - 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