buyingToBundlePiMuSigma

import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Basic

noncomputable section

/--
Seller primitives from "Buying to Bundle: Optimal Sourcing from Monopolistic
Sellers".

The model writes a buyer's value for seller `i` as `mu_i + sigma_i Z_i` in the
general item-level notation. In Theorem 4.6 the dispersion is common across
sellers, so that common-sigma case can be represented by assuming all selected
sellers have the same `sigma`.
-/
structure BuyingToBundleSeller where
  mu : Real
  sigma : Real

/--
Revenue primitives for the platform's bundle-profit set function.

`bundleRevenue S` corresponds to `Rev(v_S)`, the platform revenue from selling
the selected bundle. `monopolyRevenue mu sigma` corresponds to `Rev(mu, sigma)`,
the standalone revenue/opportunity cost of a seller with quality `mu` and
standard deviation `sigma`.
-/
structure BuyingToBundlePiMuSigmaModel where
  bundleRevenue : Finset BuyingToBundleSeller -> Real
  monopolyRevenue : Real -> Real -> Real

/--
The seller's standalone monopoly revenue/opportunity cost, `Rev(mu_i, sigma_i)`.
-/
def buyingToBundleSellerOpportunityCost
    (M : BuyingToBundlePiMuSigmaModel) (i : BuyingToBundleSeller) : Real :=
  M.monopolyRevenue i.mu i.sigma

/--
The platform's bundle-profit set function:

  Pi(S) = Rev(v_S) - sum_{i in S} Rev(mu_i, sigma_i).

This explicitly keeps each selected seller's quality `mu_i` and standard
deviation `sigma_i` in the model.
-/
def buyingToBundlePiMuSigma
    (M : BuyingToBundlePiMuSigmaModel) (S : Finset BuyingToBundleSeller) : Real :=
  M.bundleRevenue S -
    Finset.sum S (fun i => buyingToBundleSellerOpportunityCost M i)