buying_to_bundle_intermediate_surrogate_dispersion_pointwise_bound

/-
Paper source: "Buying to Bundle: Optimal Sourcing from Monopolistic Sellers",
Appendix C.2, proof of Theorem 4.6, p. 36.  This is the pointwise application
of Lemma 4.5 with `C = Upsilon(x, mu)` and `a_i = x (mu_i)`.
-/
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_buying_to_bundle_market

open MeasureTheory

theorem buying_to_bundle_intermediate_surrogate_dispersion_pointwise_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) →
      |BuyingToBundle.monopolyRevenue
          ((Measure.pi fun _ : Fin N => noise).map
            fun z => ∑ i, x (μ i) * (μ i + σ * z i)) -
        ∑ i, x (μ i) * μ i| ≤
        K * (N : ℝ) ^ ((2 : ℝ) / 3) := by sorry