buying_to_bundle_intermediate_surrogate_dispersion_pointwise_max_growth_bound
Provedasymptoticseconomicsmechanism-designprobability
Elementary growth estimate turning the four-term Lemma 4.5 maximum into a single K * N^(2/3) bound using 0 <= x <= 1 and bounded quality support.
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_dispersion_pointwise_max_growth_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 → ℝ, (∀ i, μ i ∈ Set.Icc μL μH) →
max
(max (σ * γ * Real.exp (-(1 : ℝ) / 2) *
Real.sqrt (∑ i, x (μ i) ^ 2))
(8 * σ * ξ / (3 * Real.exp 1)))
(max (Real.sqrt 2 * σ * Real.sqrt (∑ i, x (μ i) ^ 2))
(2 * σ ^ ((2 : ℝ) / 3) *
((∑ i, x (μ i) * μ i) * ∑ i, x (μ i) ^ 2) ^ ((1 : ℝ) / 3))) ≤
K * (N : ℝ) ^ ((2 : ℝ) / 3) := by sorry
Source
Buying to Bundle: Optimal Sourcing from Monopolistic Sellers, Appendix C.2, proof of Theorem 4.6