monopoly_pricing

/-
Generic monopoly-pricing primitives.

Given a buyer-value distribution `ν` on ℝ, a monopolist posting price `p` sells to the
buyers whose value is at least `p`, earning `p · ν([p, ∞))`.  The optimal monopoly
revenue is the supremum of this over all prices, and the optimal price is the price
attaining it (the largest such price, if several attain it).

These are the primitives `Rev(V)`, `Rev(μ, σ)` and `p*(μ)` of
"Buying to Bundle: Optimal Sourcing from Monopolistic Sellers" (Section 2), but they
are stated for an arbitrary value distribution so that they are reusable for any
monopoly-pricing / mechanism-design formalization.
-/
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

namespace BuyingToBundle

open MeasureTheory Set

/-- Optimal monopoly revenue for a buyer-value distribution `ν` on ℝ:
`Rev(ν) = sup_{p ∈ ℝ} p · ν([p, ∞))`.  The supremum is realized as a real `sSup`;
it is meaningful (nonempty and bounded above) whenever `ν` is a finite measure with a
finite first moment, which every theorem using it hypothesizes. -/
noncomputable def monopolyRevenue (ν : Measure ℝ) : ℝ :=
  sSup (Set.range fun p : ℝ => p * (ν (Ici p)).toReal)

/-- The optimal monopoly price for a buyer-value distribution `ν`: the largest price
attaining the optimal revenue.  When the revenue-maximizing price is unique (e.g. for
strictly regular demand), this is that unique price. -/
noncomputable def optimalPrice (ν : Measure ℝ) : ℝ :=
  sSup {p : ℝ | p * (ν (Ici p)).toReal = monopolyRevenue ν}

/-- The law of the buyer value `m + σ·Z` for an item of quality `m` and dispersion `σ`,
where `Z` is distributed according to `noise`. -/
noncomputable def valueDist (noise : Measure ℝ) (σ m : ℝ) : Measure ℝ :=
  noise.map fun z => m + σ * z

/-- `Rev(m, σ)`: the optimal monopoly revenue from selling a single item of quality `m`
to buyers with value `m + σ·Z`. -/
noncomputable def rev (noise : Measure ℝ) (σ m : ℝ) : ℝ :=
  monopolyRevenue (valueDist noise σ m)

end BuyingToBundle