buying_to_bundle_intermediate_surrogate_integrated_revenue_mean_gap_bound

Open

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

asymptoticseconomicsmechanism-designprobability

Integrated second-gap analytic bound after payment cancellation. Appendix C.2 p. 36 reduces milestone 3 to comparing the integrated monopoly revenue with the integrated deterministic mean quality.

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.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_buying_to_bundle_market

open MeasureTheory

Formal statement

theorem buying_to_bundle_intermediate_surrogate_integrated_revenue_mean_gap_bound
    (σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
    [IsProbabilityMeasure qual] [IsProbabilityMeasure noise]
    (qualPdf noisePdf : ℝ → ℝ)
    (hM : BuyingToBundle.MarketAssumptions σ μL μH γ ξ qual noise qualPdf noisePdf) :
    ∃ K : ℝ, 0 < K ∧ ∀ N : ℕ, 1 ≤ N → ∀ x : ℝ → ℝ,
      BuyingToBundle.IsAllocationRule μL μH x →
      |(∫ μ : Fin N → ℝ,
            BuyingToBundle.monopolyRevenue
              ((Measure.pi fun _ : Fin N => noise).map
                fun z => ∑ i, x (μ i) * (μ i + σ * z i))
            ∂(Measure.pi fun _ : Fin N => qual)) -
        N * ∫ m, m * x m ∂qual| ≤
        K * (N : ℝ) ^ ((2 : ℝ) / 3) := by sorry

Source

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

View graph