buying_to_bundle_virtual_cost_mul_allocation_integrable
Openasymptoticseconomicsmechanism-designprobability
Formal integrability prerequisite for the Myerson virtual-cost payment term in Appendix C.2; used to split the surrogate integral.
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
/- Paper source: "Buying to Bundle: Optimal Sourcing from Monopolistic Sellers", Lemma 4.2 and Appendix C.1. This is the formal integrability prerequisite needed to split and cancel the payment term in the proof of Theorem 4.6. -/ import Mathlib.MeasureTheory.Integral.Bochner.Basic import Definitions.Def_buying_to_bundle_market open MeasureTheory
Formal statement
theorem buying_to_bundle_virtual_cost_mul_allocation_integrable
(σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
[IsProbabilityMeasure qual] [IsProbabilityMeasure noise]
(qualPdf noisePdf : ℝ → ℝ)
(hM : BuyingToBundle.MarketAssumptions σ μL μH γ ξ qual noise qualPdf noisePdf)
(x : ℝ → ℝ) (hx : BuyingToBundle.IsAllocationRule μL μH x) :
Integrable (fun m => BuyingToBundle.virtualCost qual noise σ qualPdf m * x m) qual := by
sorry
Source
Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2, proof of Theorem 4.6