buying_to_bundle_market

/-
The incomplete-information sourcing market of
"Buying to Bundle: Optimal Sourcing from Monopolistic Sellers", Section 4.

A platform sources items from `N` monopolistic sellers.  Seller `i` has a private
quality `μᵢ`, drawn i.i.d. from a distribution `qual` with density `qualPdf` supported
on `[μL, μH]`.  A buyer values item `i` at `μᵢ + σ·Zᵢ`, where the `Zᵢ` are i.i.d. with
law `noise` (mean 0, variance 1).  The platform runs a symmetric direct mechanism with
allocation rule `x : quality → inclusion probability`; by Myerson's lemma (Lemma 4.1 of
the paper) incentive compatibility is equivalent to `x` being monotone non-increasing,
and by revenue equivalence (Lemma 4.2) the expected payment to a seller of quality `m`
is `φ(m)·x(m)` for the virtual cost `φ(m) = Rev(m,σ)·(1 + Φ(m)/(ϕ(m)·p*(m)))`.

This file defines:
* `bundleValueDist`      — the law of the bundle value `∑_{i ∈ S} (μᵢ + σZᵢ)` for a
                           fixed inclusion pattern `I`;
* `expectedBundleRevenue`— `E_{I ~ Bernoulli(x(μᵢ))}[Rev(v_{S(μ,I)})]`;
* `virtualCost`          — the Myerson virtual cost `φ`;
* `profit`               — the platform's expected profit `Π(x)` (eq. (1) of the paper);
* `surrogatePerSeller`   — the per-seller surrogate profit `ϖ(x)/N` (eq. (2));
* `IsAllocationRule`     — incentive-compatible allocation rules;
* `MarketAssumptions`    — the standing assumptions of Section 4 (densities, mean 0 /
                           variance 1 noise, strict regularity, sub-exponential tails).
-/
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Definitions.Def_monopoly_pricing

namespace BuyingToBundle

open MeasureTheory Set

/-- The law of the bundle value `∑_{i : I i} (μ i + σ * Z i)` where the qualities `μ`
and the inclusion indicators `I` are fixed and `Z : Fin N → ℝ` is i.i.d. `noise`.
This is the buyer-value distribution `v_{S(μ,I)}` of the bundle `S(μ, I) = {i | I i}`. -/
noncomputable def bundleValueDist (noise : Measure ℝ) [SigmaFinite noise] (σ : ℝ)
    {N : ℕ} (μ : Fin N → ℝ) (I : Fin N → Bool) : Measure ℝ :=
  (Measure.pi fun _ : Fin N => noise).map fun z => ∑ i, if I i then μ i + σ * z i else 0

/-- Expected optimal bundle revenue `E_{I ~ ⊗ᵢ Bernoulli(x(μᵢ))} [Rev(v_{S(μ,I)})]` for
fixed seller qualities `μ`: each seller `i` is included independently with probability
`x (μ i)`, and the platform earns the optimal monopoly revenue of the resulting bundle. -/
noncomputable def expectedBundleRevenue (noise : Measure ℝ) [SigmaFinite noise] (σ : ℝ)
    (x : ℝ → ℝ) {N : ℕ} (μ : Fin N → ℝ) : ℝ :=
  ∑ I : Fin N → Bool,
    (∏ i, if I i then x (μ i) else 1 - x (μ i)) *
      monopolyRevenue (bundleValueDist noise σ μ I)

/-- The Myerson virtual cost of a seller of quality `m` (Lemma 4.2 of the paper):
`φ(m) = Rev(m,σ) · (1 + Φ(m) / (ϕ(m) · p*(m)))`, where `Φ` is the quality cdf, `ϕ` its
density and `p*(m)` the optimal monopoly price for value distribution `m + σZ`.
The expected payment to a seller under an IC mechanism with allocation rule `x` is
`E[φ(μ)·x(μ)]`. -/
noncomputable def virtualCost (qual noise : Measure ℝ) (σ : ℝ) (qualPdf : ℝ → ℝ)
    (m : ℝ) : ℝ :=
  rev noise σ m *
    (1 + (qual (Iic m)).toReal / (qualPdf m * optimalPrice (valueDist noise σ m)))

/-- The platform's expected profit `Π(x)` from an IC mechanism with allocation rule `x`
in the `N`-seller market (eq. (1) of the paper):
`Π(x) = E_{μ ~ qual^N} [ E_{I ~ Bernoulli(x(μᵢ))} [Rev(v_{S(μ,I)})] ] - N·E_{m ~ qual}[φ(m)·x(m)]`. -/
noncomputable def profit (qual noise : Measure ℝ) [SigmaFinite qual] [SigmaFinite noise]
    (σ : ℝ) (qualPdf : ℝ → ℝ) (N : ℕ) (x : ℝ → ℝ) : ℝ :=
  (∫ μ, expectedBundleRevenue noise σ x μ ∂(Measure.pi fun _ : Fin N => qual)) -
    N * ∫ m, virtualCost qual noise σ qualPdf m * x m ∂qual

/-- The per-seller expected surrogate profit (eq. (2) of the paper divided by `N`):
`ϖ(x)/N = E_{m ~ qual}[x(m)·(m - φ(m))]`.  The surrogate replaces the bundle revenue
`Rev(v_S)` by the mean bundle quality `∑_{i ∈ S} μᵢ`. -/
noncomputable def surrogatePerSeller (qual noise : Measure ℝ) (σ : ℝ)
    (qualPdf : ℝ → ℝ) (x : ℝ → ℝ) : ℝ :=
  ∫ m, (m - virtualCost qual noise σ qualPdf m) * x m ∂qual

/-- An incentive-compatible allocation rule for the quality support `[μL, μH]`:
a measurable map into `[0,1]` that is monotone non-increasing on the support.
By Myerson's lemma (Lemma 4.1 of the paper) these are exactly the allocation rules of
IC and IR mechanisms. -/
structure IsAllocationRule (μL μH : ℝ) (x : ℝ → ℝ) : Prop where
  measurable : Measurable x
  mem_Icc : ∀ m : ℝ, x m ∈ Icc (0 : ℝ) 1
  antitoneOn : AntitoneOn x (Icc μL μH)

/-- The standing assumptions of Section 4 of the paper on the market primitives:
* `0 < σ` and `0 < μL < μH`;
* seller qualities are drawn from the probability measure `qual` with density `qualPdf`
  supported on `[μL, μH]` and positive there;
* buyer-valuation noise `Z ~ noise` is a probability measure with density `noisePdf`,
  mean `0` and variance `1`;
* `Z` is strictly regular: `η ↦ η - F̄(η)/f(η)` is strictly increasing on the support of
  the density (`F̄` the tail cdf, `f` the density) — this guarantees a unique optimal
  monopoly price and a well-defined virtual cost;
* `Z` is sub-exponential with parameters `γ, ξ > 0`:
  `E[exp(l·Z)] ≤ exp(l²γ²/2)` for all `|l| < 1/ξ` (stated as a Lebesgue integral bound
  so that it also asserts finiteness of the moment generating function). -/
structure MarketAssumptions (σ μL μH γ ξ : ℝ) (qual noise : Measure ℝ)
    (qualPdf noisePdf : ℝ → ℝ) : Prop where
  sigma_pos : 0 < σ
  muL_pos : 0 < μL
  muL_lt_muH : μL < μH
  qualPdf_meas : Measurable qualPdf
  qualPdf_nonneg : ∀ m, 0 ≤ qualPdf m
  qual_eq : qual = volume.withDensity fun m => ENNReal.ofReal (qualPdf m)
  qualPdf_support : ∀ m, m ∉ Icc μL μH → qualPdf m = 0
  qualPdf_pos : ∀ m ∈ Icc μL μH, 0 < qualPdf m
  noisePdf_meas : Measurable noisePdf
  noisePdf_nonneg : ∀ z, 0 ≤ noisePdf z
  noise_eq : noise = volume.withDensity fun z => ENNReal.ofReal (noisePdf z)
  noise_mean_zero : ∫ z, z ∂noise = 0
  noise_var_one : ∫ z, z ^ 2 ∂noise = 1
  strictly_regular :
    StrictMonoOn (fun η => η - (noise (Ici η)).toReal / noisePdf η) {η | 0 < noisePdf η}
  gamma_pos : 0 < γ
  xi_pos : 0 < ξ
  subexponential : ∀ l : ℝ, |l| < 1 / ξ →
    ∫⁻ z, ENNReal.ofReal (Real.exp (l * z)) ∂noise ≤
      ENNReal.ofReal (Real.exp (l ^ 2 * γ ^ 2 / 2))

end BuyingToBundle