buyingToBundlePi

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

noncomputable section

/--
Model data for the bundle-profit set function from
"Buying to Bundle: Optimal Sourcing from Monopolistic Sellers".

For a selected bundle `S`, `bundleRevenue S` is the revenue obtained from
selling the bundle to buyers, corresponding to `Rev(v_S)` in the paper.
For a seller `i`, `outsideOptionRevenue i` is the seller's standalone
monopoly revenue/opportunity cost, corresponding to `Rev(mu_i, sigma)`.
-/
structure BuyingToBundlePiModel (Seller : Type) where
  bundleRevenue : Finset Seller -> Real
  outsideOptionRevenue : Seller -> Real

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

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

This is a function of the selected set of sellers, not merely a function of
the market size.
-/
def buyingToBundlePi {Seller : Type}
    (M : BuyingToBundlePiModel Seller) (S : Finset Seller) : Real :=
  M.bundleRevenue S - Finset.sum S M.outsideOptionRevenue