buying_to_bundle_quality_product_ae_mem_support

Proved

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

asymptoticseconomicsmechanism-designprobability

If the quality distribution is supported on [muL, muH], then the product distribution is almost surely supported on vectors whose every coordinate lies in [muL, muH].

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 Definitions.Def_buying_to_bundle_market

open MeasureTheory

Formal statement

theorem buying_to_bundle_quality_product_ae_mem_support
    (N : ℕ) (σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
    [IsProbabilityMeasure qual] [IsProbabilityMeasure noise]
    (qualPdf noisePdf : ℝ → ℝ)
    (hM : BuyingToBundle.MarketAssumptions σ μL μH γ ξ qual noise qualPdf noisePdf) :
    ∀ᵐ μ : Fin N → ℝ ∂(Measure.pi fun _ : Fin N => qual),
      ∀ i, μ i ∈ Set.Icc μL μH := by sorry

Source

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

View graph