EconCSLib.MechanismDesign.Auction.BayesianSingleItem

Single-item auctions in incomplete-information settings, modeled as direct Bayesian mechanisms with transfers.

This file specializes the general interface from MechanismDesign/Auction/MechBayesian to the standard direct-revelation single-item auction environment:

• each agent reports a scalar type in ℝ
• the type profile is drawn from a common prior measure
• each agent receives a winning probability Q_i(t) ∈ [0,1]
• payments are determined by the mechanism's payment rule

The continuous private-value data are recorded separately via ContinuousTypeProfile, so Myerson-style regularity assumptions can be attached without forcing them into the core mechanism fields.

Interim objects are defined against an explicit family of opponent-type priors μᵢ on profiles t₋ᵢ. This keeps the generic measure-based definitions separate from any density-based formulas one may later derive under independence.

Structure hierarchy

MechanismWithTransfers I (fun _ => ℝ) (I → ℝ) ℝ
  └─ SingleParameterMechanism I ℝ                 -- allocation probabilities + payments
       └─ BayesianSingleItemAuction I             -- prior + continuous type data
            ├─ toDirectBayesianMechanismWithTransfers
            └─ toSingleParameterMechanism

structure TypeCDF (ω : ℝ) : Type

A scalar type distribution on the interval [0, ω], recorded by its CDF.

• omega_nonneg : 0 ≤ ω

  Upper bound of the support interval is nonnegative.

• cdf : ℝ → ℝ

  Cumulative distribution function.

• monotoneOn_cdf : MonotoneOn self.cdf (Set.Icc 0 ω)

  Monotonicity of the CDF on the support interval.

• cdf_zero : self.cdf 0 = 0

  Normalization at the lower endpoint.

• cdf_upper : self.cdf ω = 1

  Normalization at the upper endpoint.

• differentiableOn_cdf : DifferentiableOn ℝ self.cdf (Set.Ioo 0 ω)

  Smoothness assumption used in continuous-type auction theory.

structure ContinuousTypeProfile (I : Type u_1) : Type u_1

Agent-specific continuous private-value data.

• omega : I → ℝ

  Agent-specific upper bounds ωᵢ for the type support.

• cdf (i : I) : TypeCDF (self.omega i)

  Agent-specific CDFs Fᵢ on [0, ωᵢ].

@[reducible, inline]

abbrev OpponentProfile (I : Type u_1) (X : Type u_2) (i : I) : Type (max u_2 u_1)

Opponent profiles for agent i, with constant coordinate type X.

Equations

• OpponentProfile I X i = ({ j : I // j ≠ i } → X)

@[reducible, inline]

abbrev OpponentTypeProfile (I : Type u_1) (i : I) : Type u_1

Opponent type profiles for real-valued auction types.

Equations

• OpponentTypeProfile I i = OpponentProfile I ℝ i

structure BayesianSingleItemAuction (I : Type u_1) extends SingleParameterMechanism I ℝ : Type u_1

A direct Bayesian single-item auction with scalar private types and probabilistic allocation.

The allocation rule returns a function Q : I → ℝ, where Q i is agent i's probability of receiving the item under the reported type profile. This matches the allocation/payment shape of SingleParameterMechanism I ℝ.

The mechanism is direct: the message space equals the type space, which is taken to be ℝ for each agent, and payments are real-valued. Continuous-type data are stored separately in typeData, while the Bayesian prior is recorded by extra fields.

• allocationRule : (I → ℝ) → I → ℝ
• paymentRule : (I → ℝ) → I → ℝ
• prior : MeasureTheory.Measure (I → ℝ)

  Common prior probability measure over true type profiles.

• prob_prior : MeasureTheory.IsProbabilityMeasure self.prior

  The prior is a probability measure.

• opponentPrior (i : I) : MeasureTheory.Measure (OpponentTypeProfile I i)

  Opponent-type prior μᵢ used for interim expectations conditional on a fixed report by agent i.

• prob_opponentPrior (i : I) : MeasureTheory.IsProbabilityMeasure (self.opponentPrior i)

  Each opponent-type prior is a probability measure.

• typeData : ContinuousTypeProfile I

  Continuous private-value support and CDF data for each agent.

noncomputable def BayesianSingleItemAuction.profileInsert {I : Type u_1} {X : Type u_2} (i : I) (x : X) (t : OpponentProfile I X i) : I → X

Insert one coordinate into an opponent profile.

Equations

• BayesianSingleItemAuction.profileInsert i x t j = if h : j = i then x else t ⟨j, h⟩

@[simp]

theorem BayesianSingleItemAuction.profileInsert_self {I : Type u_1} {X : Type u_2} (i : I) (x : X) (t : OpponentProfile I X i) : profileInsert i x t i = x

The inserted coordinate is the inserted value.

@[simp]

theorem BayesianSingleItemAuction.profileInsert_of_ne {I : Type u_1} {X : Type u_2} (i : I) (x : X) (t : OpponentProfile I X i) {j : I} (hji : j ≠ i) : profileInsert i x t j = t ⟨j, hji⟩

Other coordinates come from the opponent profile.

instance BayesianSingleItemAuction.instIsProbabilityMeasureOpponentTypeProfileOpponentPrior {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) : MeasureTheory.IsProbabilityMeasure (A.opponentPrior i)

def BayesianSingleItemAuction.toDirectBayesianMechanismWithTransfers {I : Type u_1} (A : BayesianSingleItemAuction I) : DirectBayesianMechanismWithTransfers I (fun (x : I) => ℝ) (I → ℝ) ℝ

View an incomplete-information single-item auction as the corresponding direct Bayesian mechanism with transfers.

Equations

• A.toDirectBayesianMechanismWithTransfers = { prior := A.prior, prob_prior := ⋯, allocationRule := A.allocationRule, paymentRule := A.paymentRule }

@[implicit_reducible]

instance BayesianSingleItemAuction.instCoeDirectBayesianMechanismWithTransfersRealForall {I : Type u_1} : Coe (BayesianSingleItemAuction I) (DirectBayesianMechanismWithTransfers I (fun (x : I) => ℝ) (I → ℝ) ℝ)

Equations

• BayesianSingleItemAuction.instCoeDirectBayesianMechanismWithTransfersRealForall = { coe := BayesianSingleItemAuction.toDirectBayesianMechanismWithTransfers }

def BayesianSingleItemAuction.RespectsSingleItemCapacity {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) : Prop

The allocation rule respects the single-item probability budget.

Equations

• A.RespectsSingleItemCapacity = ∀ (t : I → ℝ), ∑ i : I, A.allocationRule t i ≤ 1

def BayesianSingleItemAuction.IsFeasible {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) : Prop

Feasibility for a probabilistic single-item auction:

• each winning probability lies in [0,1]
• the total allocation probability is at most 1

Equations

• A.IsFeasible = (A.IsAllocFeasible ∧ A.RespectsSingleItemCapacity)

noncomputable def BayesianSingleItemAuction.sellerRevenue {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (t : I → ℝ) : ℝ

Seller revenue at a report profile.

Equations

• A.sellerRevenue t = ∑ i : I, A.paymentRule t i

noncomputable def BayesianSingleItemAuction.expectedSellerRevenue {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) : ℝ

Ex-ante seller revenue.

Equations

• A.expectedSellerRevenue = ∫ (t : I → ℝ), A.sellerRevenue t ∂A.prior

noncomputable def BayesianSingleItemAuction.typeDensity {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) : ℝ → ℝ

Agent i's one-dimensional density, defined as the derivative of the stored CDF Fᵢ.

Equations

• A.typeDensity i = deriv (A.typeData.cdf i).cdf

noncomputable def BayesianSingleItemAuction.typeMeasure {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) : MeasureTheory.Measure ℝ

Type measure generated by fᵢ on [0, ωᵢ].

Equations

• A.typeMeasure i = (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i))).withDensity fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)

noncomputable def BayesianSingleItemAuction.jointDensity {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (t : I → ℝ) : ℝ

The joint density f(t) of the type profile under independence.

If the agents' types are independent with agent-specific one-dimensional densities fᵢ, then the profile density is the product ∏ᵢ fᵢ(tᵢ).

Equations

• A.jointDensity t = ∏ i : I, A.typeDensity i (t i)

noncomputable def BayesianSingleItemAuction.productPrior {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) : MeasureTheory.Measure (I → ℝ)

Product type prior.

Equations

• A.productPrior = MeasureTheory.Measure.pi fun (i : I) => A.typeMeasure i

noncomputable def BayesianSingleItemAuction.opponentProductPrior {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) (i : I) : MeasureTheory.Measure (OpponentTypeProfile I i)

Product prior over i's opponents.

Equations

• A.opponentProductPrior i = MeasureTheory.Measure.pi fun (j : { j : I // j ≠ i }) => A.typeMeasure ↑j

def BayesianSingleItemAuction.HasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) : Prop

Stored priors are the product priors.

Equations

• A.HasIndependentTypePriors = (A.prior = A.productPrior ∧ ∀ (i : I), A.opponentPrior i = A.opponentProductPrior i)

def BayesianSingleItemAuction.HasSameSellingEnvironment {I : Type u_1} (A B : BayesianSingleItemAuction I) : Prop

Auctions over the same Bayesian selling environment.

Equations

• A.HasSameSellingEnvironment B = (B.prior = A.prior ∧ B.opponentPrior = A.opponentPrior ∧ B.typeData = A.typeData)

theorem BayesianSingleItemAuction.HasSameSellingEnvironment.prior_eq {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.HasSameSellingEnvironment B) : B.prior = A.prior

theorem BayesianSingleItemAuction.HasSameSellingEnvironment.opponentPrior_eq {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.HasSameSellingEnvironment B) : B.opponentPrior = A.opponentPrior

theorem BayesianSingleItemAuction.HasSameSellingEnvironment.typeData_eq {I : Type u_1} {A B : BayesianSingleItemAuction I} (h : A.HasSameSellingEnvironment B) : B.typeData = A.typeData

instance BayesianSingleItemAuction.productPrior_isProbabilityMeasure {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] : MeasureTheory.IsProbabilityMeasure A.productPrior

instance BayesianSingleItemAuction.opponentProductPrior_isProbabilityMeasure {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) (i : I) [∀ (j : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure j)] : MeasureTheory.IsProbabilityMeasure (A.opponentProductPrior i)

theorem BayesianSingleItemAuction.productPrior_map_eval {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) : MeasureTheory.Measure.map (Function.eval i) A.productPrior = A.typeMeasure i

theorem BayesianSingleItemAuction.opponentProductPrior_map_eval {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) (j : { j : I // j ≠ i }) : MeasureTheory.Measure.map (Function.eval j) (A.opponentProductPrior i) = A.typeMeasure ↑j

theorem BayesianSingleItemAuction.prior_map_eval_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) (i : I) : MeasureTheory.Measure.map (Function.eval i) A.prior = A.typeMeasure i

theorem BayesianSingleItemAuction.opponentPrior_map_eval_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) (i : I) (j : { j : I // j ≠ i }) : MeasureTheory.Measure.map (Function.eval j) (A.opponentPrior i) = A.typeMeasure ↑j

theorem BayesianSingleItemAuction.integrable_comp_eval_productPrior {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] {i : I} {E : Type u_2} [NormedAddCommGroup E] {f : ℝ → E} (hf : MeasureTheory.Integrable f (A.typeMeasure i)) : MeasureTheory.Integrable (fun (t : I → ℝ) => f (t i)) A.productPrior

theorem BayesianSingleItemAuction.integrable_comp_eval_opponentProductPrior {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] {i : I} {j : { j : I // j ≠ i }} {E : Type u_2} [NormedAddCommGroup E] {f : ℝ → E} (hf : MeasureTheory.Integrable f (A.typeMeasure ↑j)) : MeasureTheory.Integrable (fun (t : OpponentTypeProfile I i) => f (t j)) (A.opponentProductPrior i)

theorem BayesianSingleItemAuction.integral_comp_eval_productPrior {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] {i : I} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : MeasureTheory.AEStronglyMeasurable f (A.typeMeasure i)) : ∫ (t : I → ℝ), f (t i) ∂A.productPrior = ∫ (v : ℝ), f v ∂A.typeMeasure i

theorem BayesianSingleItemAuction.integral_comp_eval_opponentProductPrior {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] {i : I} {j : { j : I // j ≠ i }} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : MeasureTheory.AEStronglyMeasurable f (A.typeMeasure ↑j)) : ∫ (t : OpponentTypeProfile I i), f (t j) ∂A.opponentProductPrior i = ∫ (v : ℝ), f v ∂A.typeMeasure ↑j

theorem BayesianSingleItemAuction.integrable_comp_eval_prior_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) {i : I} {E : Type u_2} [NormedAddCommGroup E] {f : ℝ → E} (hf : MeasureTheory.Integrable f (A.typeMeasure i)) : MeasureTheory.Integrable (fun (t : I → ℝ) => f (t i)) A.prior

theorem BayesianSingleItemAuction.integrable_comp_eval_opponentPrior_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) {i : I} {j : { j : I // j ≠ i }} {E : Type u_2} [NormedAddCommGroup E] {f : ℝ → E} (hf : MeasureTheory.Integrable f (A.typeMeasure ↑j)) : MeasureTheory.Integrable (fun (t : OpponentTypeProfile I i) => f (t j)) (A.opponentPrior i)

theorem BayesianSingleItemAuction.integral_comp_eval_prior_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) {i : I} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : MeasureTheory.AEStronglyMeasurable f (A.typeMeasure i)) : ∫ (t : I → ℝ), f (t i) ∂A.prior = ∫ (v : ℝ), f v ∂A.typeMeasure i

theorem BayesianSingleItemAuction.integral_comp_eval_opponentPrior_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) {i : I} {j : { j : I // j ≠ i }} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} (hf : MeasureTheory.AEStronglyMeasurable f (A.typeMeasure ↑j)) : ∫ (t : OpponentTypeProfile I i), f (t j) ∂A.opponentPrior i = ∫ (v : ℝ), f v ∂A.typeMeasure ↑j

theorem BayesianSingleItemAuction.integral_typeMeasure_eq_intervalIntegral_smul {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : ℝ → E) (hmeas : AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))) (hnonneg : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) : ∫ (v : ℝ), g v ∂A.typeMeasure i = ∫ (v : ℝ) in 0..A.typeData.omega i, A.typeDensity i v • g v

Integral against typeMeasure as an interval integral.

theorem BayesianSingleItemAuction.integral_typeMeasure_eq_intervalIntegral_mul {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (g : ℝ → ℝ) (hmeas : AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))) (hnonneg : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) : ∫ (v : ℝ), g v ∂A.typeMeasure i = ∫ (v : ℝ) in 0..A.typeData.omega i, g v * A.typeDensity i v

Real-valued form of integral_typeMeasure_eq_intervalIntegral_smul.

noncomputable def BayesianSingleItemAuction.reportProfile {I : Type u_1} (i : I) (z_i : ℝ) (t : OpponentTypeProfile I i) : I → ℝ

The reported type profile obtained by combining zᵢ with an opponent profile t₋ᵢ.

Equations

• BayesianSingleItemAuction.reportProfile i z_i t = BayesianSingleItemAuction.profileInsert i z_i t

@[simp]

theorem BayesianSingleItemAuction.reportProfile_self {I : Type u_1} (i : I) (z_i : ℝ) (t : OpponentTypeProfile I i) : reportProfile i z_i t i = z_i

The inserted coordinate is zᵢ.

@[simp]

theorem BayesianSingleItemAuction.reportProfile_of_ne {I : Type u_1} (i : I) (z_i : ℝ) (t : OpponentTypeProfile I i) {j : I} (hji : j ≠ i) : reportProfile i z_i t j = t ⟨j, hji⟩

Other coordinates come from the opponent profile.

@[simp]

theorem BayesianSingleItemAuction.update_reportProfile_self {I : Type u_1} [DecidableEq I] (i : I) (z_i y_i : ℝ) (t : OpponentTypeProfile I i) : Function.update (reportProfile i z_i t) i y_i = reportProfile i y_i t

Updating coordinate i replaces the inserted report.

noncomputable def BayesianSingleItemAuction.profileSplitMeasurableEquiv {I : Type u_1} (i : I) : (I → ℝ) ≃ᵐ ℝ × OpponentTypeProfile I i

Split a profile into coordinate i and its opponents.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BayesianSingleItemAuction.profileSplitMeasurableEquiv_apply_fst {I : Type u_1} (i : I) (t : I → ℝ) : ((profileSplitMeasurableEquiv i) t).1 = t i

@[simp]

theorem BayesianSingleItemAuction.profileSplitMeasurableEquiv_apply_snd {I : Type u_1} (i : I) (t : I → ℝ) (j : { j : I // j ≠ i }) : ((profileSplitMeasurableEquiv i) t).2 j = t ↑j

@[simp]

theorem BayesianSingleItemAuction.profileSplitMeasurableEquiv_symm_apply {I : Type u_1} (i : I) (v : ℝ) (t : OpponentTypeProfile I i) : (profileSplitMeasurableEquiv i).symm (v, t) = reportProfile i v t

theorem BayesianSingleItemAuction.measurePreserving_profileSplitMeasurableEquiv_productPrior {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) : MeasureTheory.MeasurePreserving (⇑(profileSplitMeasurableEquiv i)) A.productPrior ((A.typeMeasure i).prod (A.opponentProductPrior i))

theorem BayesianSingleItemAuction.productPrior_map_profileSplitMeasurableEquiv {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) : MeasureTheory.Measure.map (⇑(profileSplitMeasurableEquiv i)) A.productPrior = (A.typeMeasure i).prod (A.opponentProductPrior i)

theorem BayesianSingleItemAuction.prior_map_profileSplitMeasurableEquiv_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) (i : I) : MeasureTheory.Measure.map (⇑(profileSplitMeasurableEquiv i)) A.prior = (A.typeMeasure i).prod (A.opponentProductPrior i)

theorem BayesianSingleItemAuction.integral_comp_profileSplitMeasurableEquiv_productPrior {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : ℝ × OpponentTypeProfile I i → E) : ∫ (t : I → ℝ), g ((profileSplitMeasurableEquiv i) t) ∂A.productPrior = ∫ (p : ℝ × OpponentTypeProfile I i), g p ∂(A.typeMeasure i).prod (A.opponentProductPrior i)

theorem BayesianSingleItemAuction.integrable_productPrior_of_integrable_profileSplit {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) {E : Type u_2} [NormedAddCommGroup E] {f : (I → ℝ) → E} (hf : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => f (reportProfile i p.1 p.2)) ((A.typeMeasure i).prod (A.opponentProductPrior i))) : MeasureTheory.Integrable f A.productPrior

theorem BayesianSingleItemAuction.integrable_prior_of_integrable_profileSplit_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) (i : I) {E : Type u_2} [NormedAddCommGroup E] {f : (I → ℝ) → E} (hf : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => f (reportProfile i p.1 p.2)) ((A.typeMeasure i).prod (A.opponentPrior i))) : MeasureTheory.Integrable f A.prior

theorem BayesianSingleItemAuction.integral_productPrior_eq_integral_typeMeasure_opponentProductPrior {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (i : I) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (I → ℝ) → E) (hf : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => f (reportProfile i p.1 p.2)) ((A.typeMeasure i).prod (A.opponentProductPrior i))) : ∫ (t : I → ℝ), f t ∂A.productPrior = ∫ (v : ℝ), ∫ (t : OpponentTypeProfile I i), f (reportProfile i v t) ∂A.opponentProductPrior i ∂A.typeMeasure i

Fubini decomposition under the product prior.

theorem BayesianSingleItemAuction.integral_prior_eq_integral_typeMeasure_opponentProductPrior_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) (i : I) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (I → ℝ) → E) (hf : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => f (reportProfile i p.1 p.2)) ((A.typeMeasure i).prod (A.opponentProductPrior i))) : ∫ (t : I → ℝ), f t ∂A.prior = ∫ (v : ℝ), ∫ (t : OpponentTypeProfile I i), f (reportProfile i v t) ∂A.opponentProductPrior i ∂A.typeMeasure i

theorem BayesianSingleItemAuction.integral_prior_eq_integral_typeMeasure_opponentPrior_of_hasIndependentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] (A : BayesianSingleItemAuction I) [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (h : A.HasIndependentTypePriors) (i : I) {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : (I → ℝ) → E) (hf : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => f (reportProfile i p.1 p.2)) ((A.typeMeasure i).prod (A.opponentPrior i))) : ∫ (t : I → ℝ), f t ∂A.prior = ∫ (v : ℝ), ∫ (t : OpponentTypeProfile I i), f (reportProfile i v t) ∂A.opponentPrior i ∂A.typeMeasure i

noncomputable def BayesianSingleItemAuction.interimExpectation {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) (f : (I → ℝ) → ℝ) : ℝ

Interim expectation of a full-profile observable after report zᵢ.

Equations

• A.interimExpectation i z_i f = ∫ (t : OpponentTypeProfile I i), f (BayesianSingleItemAuction.reportProfile i z_i t) ∂A.opponentPrior i

noncomputable def BayesianSingleItemAuction.interimAllocationIntegrand {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) (t : OpponentTypeProfile I i) : ℝ

Allocation integrand for interim probability.

Equations

• A.interimAllocationIntegrand i z_i t = A.allocationRule (BayesianSingleItemAuction.reportProfile i z_i t) i

noncomputable def BayesianSingleItemAuction.interimPaymentIntegrand {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) (t : OpponentTypeProfile I i) : ℝ

Payment integrand for interim payment.

Equations

• A.interimPaymentIntegrand i z_i t = A.paymentRule (BayesianSingleItemAuction.reportProfile i z_i t) i

noncomputable def BayesianSingleItemAuction.interimQuasiLinearUtilityIntegrand {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (t_i z_i : ℝ) (t : OpponentTypeProfile I i) : ℝ

Quasi-linear utility integrand.

Equations

• A.interimQuasiLinearUtilityIntegrand i t_i z_i t = t_i * A.interimAllocationIntegrand i z_i t - A.interimPaymentIntegrand i z_i t

def BayesianSingleItemAuction.HasIntegrableInterimAllocation {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Allocation integrands are integrable.

Equations

• A.HasIntegrableInterimAllocation = ∀ (i : I) (z_i : ℝ), MeasureTheory.Integrable (fun (t : OpponentTypeProfile I i) => A.interimAllocationIntegrand i z_i t) (A.opponentPrior i)

def BayesianSingleItemAuction.HasIntegrableInterimPayment {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Payment integrands are integrable.

Equations

• A.HasIntegrableInterimPayment = ∀ (i : I) (z_i : ℝ), MeasureTheory.Integrable (fun (t : OpponentTypeProfile I i) => A.interimPaymentIntegrand i z_i t) (A.opponentPrior i)

def BayesianSingleItemAuction.HasIntegrableInterimObjects {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Allocation and payment integrability.

Equations

• A.HasIntegrableInterimObjects = (A.HasIntegrableInterimAllocation ∧ A.HasIntegrableInterimPayment)

theorem BayesianSingleItemAuction.hasIntegrableInterimAllocation_of_aestronglyMeasurable_of_bound {I : Type u_1} (A : BayesianSingleItemAuction I) (hmeas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.interimAllocationIntegrand i z_i t) (A.opponentPrior i)) (hbound : ∀ (i : I) (z_i : ℝ), ∃ (C : ℝ), ∀ᵐ (t : OpponentTypeProfile I i) ∂A.opponentPrior i, ‖A.interimAllocationIntegrand i z_i t‖ ≤ C) : A.HasIntegrableInterimAllocation

Bounded a.e. strongly measurable allocation integrands are integrable.

theorem BayesianSingleItemAuction.hasIntegrableInterimPayment_of_aestronglyMeasurable_of_bound {I : Type u_1} (A : BayesianSingleItemAuction I) (hmeas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.interimPaymentIntegrand i z_i t) (A.opponentPrior i)) (hbound : ∀ (i : I) (z_i : ℝ), ∃ (C : ℝ), ∀ᵐ (t : OpponentTypeProfile I i) ∂A.opponentPrior i, ‖A.interimPaymentIntegrand i z_i t‖ ≤ C) : A.HasIntegrableInterimPayment

Bounded a.e. strongly measurable payment integrands are integrable.

theorem BayesianSingleItemAuction.hasIntegrableInterimObjects_of_aestronglyMeasurable_of_bound {I : Type u_1} (A : BayesianSingleItemAuction I) (halloc_meas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.interimAllocationIntegrand i z_i t) (A.opponentPrior i)) (hpay_meas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.interimPaymentIntegrand i z_i t) (A.opponentPrior i)) (halloc_bound : ∀ (i : I) (z_i : ℝ), ∃ (C : ℝ), ∀ᵐ (t : OpponentTypeProfile I i) ∂A.opponentPrior i, ‖A.interimAllocationIntegrand i z_i t‖ ≤ C) (hpay_bound : ∀ (i : I) (z_i : ℝ), ∃ (C : ℝ), ∀ᵐ (t : OpponentTypeProfile I i) ∂A.opponentPrior i, ‖A.interimPaymentIntegrand i z_i t‖ ≤ C) : A.HasIntegrableInterimObjects

A.e. strong measurability and bounds imply interim integrability.

theorem BayesianSingleItemAuction.hasIntegrableInterimAllocation_of_isFeasible_of_aestronglyMeasurable {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (hfeas : A.IsFeasible) (hmeas : ∀ (i : I) (z_i : ℝ), MeasureTheory.AEStronglyMeasurable (fun (t : OpponentTypeProfile I i) => A.interimAllocationIntegrand i z_i t) (A.opponentPrior i)) : A.HasIntegrableInterimAllocation

Feasibility and a.e. strong measurability imply allocation integrability.

noncomputable def BayesianSingleItemAuction.interimAllocProb {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) : ℝ

Interim allocation probability q_i(z_i).

Equations

• A.interimAllocProb i z_i = A.interimExpectation i z_i fun (r : I → ℝ) => A.allocationRule r i

noncomputable def BayesianSingleItemAuction.interimExpectedPayment {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) : ℝ

Interim expected payment m_i(z_i).

Equations

• A.interimExpectedPayment i z_i = A.interimExpectation i z_i fun (r : I → ℝ) => A.paymentRule r i

theorem BayesianSingleItemAuction.interimAllocProb_eq_integral_interimAllocationIntegrand {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) : A.interimAllocProb i z_i = ∫ (t : OpponentTypeProfile I i), A.interimAllocationIntegrand i z_i t ∂A.opponentPrior i

The generic interim expectation specializes to the allocation integrand.

theorem BayesianSingleItemAuction.interimExpectedPayment_eq_integral_interimPaymentIntegrand {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (z_i : ℝ) : A.interimExpectedPayment i z_i = ∫ (t : OpponentTypeProfile I i), A.interimPaymentIntegrand i z_i t ∂A.opponentPrior i

The generic interim expectation specializes to the payment integrand.

theorem BayesianSingleItemAuction.intervalIntegrable_interimExpectedPayment_mul_typeDensity_of_profileSplit_integrable {I : Type u_1} {A B : BayesianSingleItemAuction I} (i : I) (hmeas : AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))) (hnonneg : ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hpay : MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.paymentRule (reportProfile i p.1 p.2) i) ((A.typeMeasure i).prod (B.opponentPrior i))) : IntervalIntegrable (fun (v : ℝ) => B.interimExpectedPayment i v * A.typeDensity i v) MeasureTheory.volume 0 (A.typeData.omega i)

Product-side integrability gives interval integrability of m_i f_i.

theorem BayesianSingleItemAuction.interimAllocProb_nonneg_of_isFeasible {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (hfeas : A.IsFeasible) (i : I) (z_i : ℝ) : 0 ≤ A.interimAllocProb i z_i

Feasible auctions have nonnegative interim allocation probabilities.

theorem BayesianSingleItemAuction.interimAllocProb_le_one_of_isFeasible {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (hfeas : A.IsFeasible) (hint : A.HasIntegrableInterimAllocation) (i : I) (z_i : ℝ) : A.interimAllocProb i z_i ≤ 1

Feasible auctions have interim allocation probabilities at most 1.

theorem BayesianSingleItemAuction.interimAllocProb_mem_Icc_of_isFeasible {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (hfeas : A.IsFeasible) (hint : A.HasIntegrableInterimAllocation) (i : I) (z_i : ℝ) : A.interimAllocProb i z_i ∈ Set.Icc 0 1

Feasible interim allocation probabilities lie in [0, 1].

Payment revenue through interim payments

noncomputable def BayesianSingleItemAuction.expectedPaymentRevenueInEnvironment {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (p : (I → ℝ) → I → ℝ) : ℝ

Expected total payment revenue under the base prior.

Equations

• A.expectedPaymentRevenueInEnvironment p = ∫ (t : I → ℝ), ∑ i : I, p t i ∂A.prior

noncomputable def BayesianSingleItemAuction.expectedSellerRevenueInEnvironment {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : ℝ

Expected seller revenue of B, evaluated in environment A.

Equations

• A.expectedSellerRevenueInEnvironment B = A.expectedPaymentRevenueInEnvironment B.paymentRule

noncomputable def BayesianSingleItemAuction.expectedInterimPaymentRevenue {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : ℝ

Ex-ante revenue through interim expected payments.

Equations

• A.expectedInterimPaymentRevenue B = ∑ i : I, ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimExpectedPayment i v * A.typeDensity i v

@[simp]

theorem BayesianSingleItemAuction.expectedSellerRevenueInEnvironment_self {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) : A.expectedSellerRevenueInEnvironment A = A.expectedSellerRevenue

def BayesianSingleItemAuction.HasExpectedRevenueInterimPaymentIdentity {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Ex-ante revenue agrees with the interim-payment expression.

Equations

• A.HasExpectedRevenueInterimPaymentIdentity B = (A.expectedSellerRevenueInEnvironment B = A.expectedInterimPaymentRevenue B)

structure BayesianSingleItemAuction.PaymentInterimFubiniAssumptions {I : Type u_1} [Fintype I] (A B : BayesianSingleItemAuction I) : Prop

Payment-side Fubini hypotheses connecting ex-ante and interim expressions.

• payment_integrable (i : I) : MeasureTheory.Integrable (fun (t : I → ℝ) => B.paymentRule t i) A.prior
• payment_interim_fubini (i : I) : ∫ (t : I → ℝ), B.paymentRule t i ∂A.prior = ∫ (v : ℝ) in 0..A.typeData.omega i, B.interimExpectedPayment i v * A.typeDensity i v

theorem BayesianSingleItemAuction.PaymentInterimFubiniAssumptions.expectedPaymentRevenueIntegrable {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.PaymentInterimFubiniAssumptions B) : MeasureTheory.Integrable (fun (t : I → ℝ) => ∑ i : I, B.paymentRule t i) A.prior

theorem BayesianSingleItemAuction.PaymentInterimFubiniAssumptions.hasExpectedRevenueInterimPaymentIdentity {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (h : A.PaymentInterimFubiniAssumptions B) : A.HasExpectedRevenueInterimPaymentIdentity B

theorem BayesianSingleItemAuction.paymentInterimFubiniAssumptions_of_typeMeasure_fubini {I : Type u_1} [Fintype I] {A B : BayesianSingleItemAuction I} (hdens_meas : ∀ (i : I), AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))) (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hpay_int : ∀ (i : I), MeasureTheory.Integrable (fun (t : I → ℝ) => B.paymentRule t i) A.prior) (hpay_fubini : ∀ (i : I), ∫ (t : I → ℝ), B.paymentRule t i ∂A.prior = ∫ (v : ℝ), B.interimExpectedPayment i v ∂A.typeMeasure i) : A.PaymentInterimFubiniAssumptions B

Build payment-side interim Fubini hypotheses from type-measure Fubini.

theorem BayesianSingleItemAuction.paymentInterimFubiniAssumptions_of_independentTypePriors {I : Type u_1} [Fintype I] [DecidableEq I] {A B : BayesianSingleItemAuction I} [∀ (i : I), MeasureTheory.IsProbabilityMeasure (A.typeMeasure i)] (hdens_meas : ∀ (i : I), AEMeasurable (fun (v : ℝ) => ENNReal.ofReal (A.typeDensity i v)) (MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)))) (hdens_ae : ∀ (i : I), ∀ᵐ (v : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 (A.typeData.omega i)), 0 ≤ A.typeDensity i v) (hind : A.HasIndependentTypePriors) (henv : A.HasSameSellingEnvironment B) (hpay_prod_int : ∀ (i : I), MeasureTheory.Integrable (fun (p : ℝ × OpponentTypeProfile I i) => B.paymentRule (reportProfile i p.1 p.2) i) ((A.typeMeasure i).prod (B.opponentPrior i))) : A.PaymentInterimFubiniAssumptions B

Independent priors and product-side payment integrability imply the payment-side interim Fubini package.

def BayesianSingleItemAuction.HasIntervalIntegrableInterimAllocationOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Supportwise interval integrability of q_i.

Equations

• A.HasIntervalIntegrableInterimAllocationOnSupport = ∀ (i : I), IntervalIntegrable (A.interimAllocProb i) MeasureTheory.volume 0 (A.typeData.omega i)

def BayesianSingleItemAuction.HasIntervalIntegrableInterimAllocation {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Global interval integrability of q_i.

Equations

• A.HasIntervalIntegrableInterimAllocation = ∀ (i : I) (a b : ℝ), IntervalIntegrable (A.interimAllocProb i) MeasureTheory.volume a b

noncomputable def BayesianSingleItemAuction.interimQuasiLinearUtility {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (t_i z_i : ℝ) : ℝ

Interim utility q_i(z_i) * t_i - m_i(z_i).

Equations

• A.interimQuasiLinearUtility i t_i z_i = A.interimAllocProb i z_i * t_i - A.interimExpectedPayment i z_i

noncomputable def BayesianSingleItemAuction.equilibriumPayoff {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (t_i : ℝ) : ℝ

Truthful interim payoff U_i(t_i).

Equations

• A.equilibriumPayoff i t_i = A.interimQuasiLinearUtility i t_i t_i

def BayesianSingleItemAuction.IsIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Interim incentive compatibility.

Equations

• A.IsIncentiveCompatible = ∀ (i : I) (t_i z_i : ℝ), A.interimQuasiLinearUtility i t_i z_i ≤ A.equilibriumPayoff i t_i

theorem BayesianSingleItemAuction.interimQuasiLinearUtility_eq_equilibriumPayoff_add {I : Type u_1} (A : BayesianSingleItemAuction I) (i : I) (t_i z_i : ℝ) : A.interimQuasiLinearUtility i t_i z_i = A.equilibriumPayoff i z_i + A.interimAllocProb i z_i * (t_i - z_i)

Misreport utility in terms of truthful payoff at the report.

theorem BayesianSingleItemAuction.integrable_interimQuasiLinearUtilityIntegrand {I : Type u_1} (A : BayesianSingleItemAuction I) (hQ : A.HasIntegrableInterimAllocation) (hM : A.HasIntegrableInterimPayment) (i : I) (t_i z_i : ℝ) : MeasureTheory.Integrable (fun (t : OpponentTypeProfile I i) => A.interimQuasiLinearUtilityIntegrand i t_i z_i t) (A.opponentPrior i)

Utility integrability from allocation and payment integrability.

theorem BayesianSingleItemAuction.integral_interimQuasiLinearUtilityIntegrand_eq {I : Type u_1} (A : BayesianSingleItemAuction I) (hQ : A.HasIntegrableInterimAllocation) (hM : A.HasIntegrableInterimPayment) (i : I) (t_i z_i : ℝ) : ∫ (t : OpponentTypeProfile I i), A.interimQuasiLinearUtilityIntegrand i t_i z_i t ∂A.opponentPrior i = A.interimQuasiLinearUtility i t_i z_i

The utility integrand integrates to interim utility.

theorem BayesianSingleItemAuction.interimQuasiLinearUtilityIntegrand_le_of_isDSIC {I : Type u_1} [DecidableEq I] (A : BayesianSingleItemAuction I) (hdsic : A.IsDSIC) (i : I) (t_i z_i : ℝ) (t : OpponentTypeProfile I i) : A.interimQuasiLinearUtilityIntegrand i t_i z_i t ≤ A.interimQuasiLinearUtilityIntegrand i t_i t_i t

Pointwise DSIC inequality for the interim utility integrand.

theorem BayesianSingleItemAuction.isIncentiveCompatible_of_isDSIC {I : Type u_1} [DecidableEq I] (A : BayesianSingleItemAuction I) (hint : A.HasIntegrableInterimObjects) (hdsic : A.IsDSIC) : A.IsIncentiveCompatible

DSIC implies interim IC under interim integrability.

theorem BayesianSingleItemAuction.isIncentiveCompatible_iff_equilibriumPayoff_ge {I : Type u_1} (A : BayesianSingleItemAuction I) : A.IsIncentiveCompatible ↔ ∀ (i : I) (v_i x_i : ℝ), A.equilibriumPayoff i v_i ≥ A.equilibriumPayoff i x_i + A.interimAllocProb i x_i * (v_i - x_i)

[MSZ 12.48] IC iff the one-dimensional payoff inequality.

theorem BayesianSingleItemAuction.interimAllocProb_mono_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) (i : I) : Monotone (A.interimAllocProb i)

IC implies monotonicity of q_i.

theorem BayesianSingleItemAuction.hasIntervalIntegrableInterimAllocation_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) : A.HasIntervalIntegrableInterimAllocation

IC gives global interval integrability of q_i.

theorem BayesianSingleItemAuction.equilibriumPayoff_convexOn_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) (i : I) : ConvexOn ℝ Set.univ (A.equilibriumPayoff i)

IC makes truthful payoff convex.

theorem BayesianSingleItemAuction.deriv_equilibriumPayoff_eq_interimAllocProb_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) {i : I} {v_i : ℝ} (hdiff : DifferentiableAt ℝ (A.equilibriumPayoff i) v_i) : deriv (A.equilibriumPayoff i) v_i = A.interimAllocProb i v_i

At differentiable types, U_i' = q_i.

def BayesianSingleItemAuction.IsIndividuallyRational {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Interim individual rationality.

Equations

• A.IsIndividuallyRational = ∀ (i : I) (t_i : ℝ), 0 ≤ A.equilibriumPayoff i t_i

def BayesianSingleItemAuction.IsIndividuallyRationalOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Interim individual rationality on [0, ωᵢ].

Equations

• A.IsIndividuallyRationalOnSupport = ∀ (i : I) (t_i : ℝ), 0 ≤ t_i → t_i ≤ A.typeData.omega i → 0 ≤ A.equilibriumPayoff i t_i

def BayesianSingleItemAuction.HasInterimEnvelopeFormula {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

[MSZ 12.49] Payoff envelope.

Equations

• A.HasInterimEnvelopeFormula = ∀ (i : I) (v_i : ℝ), A.equilibriumPayoff i v_i = A.equilibriumPayoff i 0 + ∫ (z : ℝ) in 0..v_i, A.interimAllocProb i z

def BayesianSingleItemAuction.HasInterimPaymentFormula {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

[MSZ 12.49] Payment identity.

Equations

• One or more equations did not get rendered due to their size.

def BayesianSingleItemAuction.HasInterimEnvelopeDerivative {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Envelope derivative condition.

Equations

• A.HasInterimEnvelopeDerivative = ∀ (i : I) (v_i : ℝ), HasDerivAt (A.equilibriumPayoff i) (A.interimAllocProb i v_i) v_i

theorem BayesianSingleItemAuction.hasInterimEnvelopeDerivative_of_isIncentiveCompatible_of_equilibriumPayoff_differentiable {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) (hdiff : ∀ (i : I) (v_i : ℝ), DifferentiableAt ℝ (A.equilibriumPayoff i) v_i) : A.HasInterimEnvelopeDerivative

IC and differentiability give the envelope derivative.

theorem BayesianSingleItemAuction.hasInterimEnvelopeFormula_of_hasInterimEnvelopeDerivative {I : Type u_1} (A : BayesianSingleItemAuction I) (hderiv : A.HasInterimEnvelopeDerivative) (hint : A.HasIntervalIntegrableInterimAllocation) : A.HasInterimEnvelopeFormula

The envelope derivative gives the payoff envelope.

theorem BayesianSingleItemAuction.hasInterimEnvelopeFormula_of_isIncentiveCompatible_of_hasInterimEnvelopeDerivative {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) (hderiv : A.HasInterimEnvelopeDerivative) : A.HasInterimEnvelopeFormula

IC plus the envelope derivative gives the payoff envelope.

theorem BayesianSingleItemAuction.hasInterimEnvelopeFormula_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) : A.HasInterimEnvelopeFormula

[MSZ 12.49] Payoff envelope from IC.

theorem BayesianSingleItemAuction.equilibriumPayoff_eq_neg_interimExpectedPayment_zero_add_integral {I : Type u_1} (A : BayesianSingleItemAuction I) (henv : A.HasInterimEnvelopeFormula) (i : I) (v_i : ℝ) : A.equilibriumPayoff i v_i = -A.interimExpectedPayment i 0 + ∫ (z : ℝ) in 0..v_i, A.interimAllocProb i z

[MSZ 12.146] Payoff identity.

theorem BayesianSingleItemAuction.hasInterimPaymentFormula_of_hasInterimEnvelopeFormula {I : Type u_1} (A : BayesianSingleItemAuction I) (henv : A.HasInterimEnvelopeFormula) : A.HasInterimPaymentFormula

The payoff envelope implies the payment identity.

theorem BayesianSingleItemAuction.hasInterimPaymentFormula_of_hasInterimEnvelopeDerivative {I : Type u_1} (A : BayesianSingleItemAuction I) (hderiv : A.HasInterimEnvelopeDerivative) (hint : A.HasIntervalIntegrableInterimAllocation) : A.HasInterimPaymentFormula

The envelope derivative implies the payment identity.

theorem BayesianSingleItemAuction.hasInterimPaymentFormula_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) : A.HasInterimPaymentFormula

[MSZ 12.147] Payment identity from IC.

theorem BayesianSingleItemAuction.interimEnvelopeFormula_and_paymentFormula_of_isIncentiveCompatible_of_hasInterimEnvelopeDerivative {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) (hderiv : A.HasInterimEnvelopeDerivative) : A.HasInterimEnvelopeFormula ∧ A.HasInterimPaymentFormula

Envelope and payment identities from IC and the derivative condition.

theorem BayesianSingleItemAuction.interimEnvelopeFormula_and_paymentFormula_of_isIncentiveCompatible {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) : A.HasInterimEnvelopeFormula ∧ A.HasInterimPaymentFormula

[MSZ 12.49] Envelope and payment identities from IC.

theorem BayesianSingleItemAuction.equilibriumPayoff_eq_of_hasInterimEnvelopeFormula_of_interimAllocProb_eq {I : Type u_1} (A B : BayesianSingleItemAuction I) (henvA : A.HasInterimEnvelopeFormula) (henvB : B.HasInterimEnvelopeFormula) (i : I) (hQ : ∀ (z : ℝ), A.interimAllocProb i z = B.interimAllocProb i z) (hM0 : A.interimExpectedPayment i 0 = B.interimExpectedPayment i 0) (v_i : ℝ) : A.equilibriumPayoff i v_i = B.equilibriumPayoff i v_i

Same q_i and zero-type payment give the same truthful payoff.

theorem BayesianSingleItemAuction.interimExpectedPayment_eq_of_hasInterimPaymentFormula_of_interimAllocProb_eq {I : Type u_1} (A B : BayesianSingleItemAuction I) (hpayA : A.HasInterimPaymentFormula) (hpayB : B.HasInterimPaymentFormula) (i : I) (hQ : ∀ (z : ℝ), A.interimAllocProb i z = B.interimAllocProb i z) (hM0 : A.interimExpectedPayment i 0 = B.interimExpectedPayment i 0) (v_i : ℝ) : A.interimExpectedPayment i v_i = B.interimExpectedPayment i v_i

Same q_i and zero-type payment give the same interim payment.

theorem BayesianSingleItemAuction.interimExpectedPayment_eq_and_equilibriumPayoff_eq_of_hasInterimEnvelopeFormula {I : Type u_1} (A B : BayesianSingleItemAuction I) (henvA : A.HasInterimEnvelopeFormula) (henvB : B.HasInterimEnvelopeFormula) (i : I) (hQ : ∀ (z : ℝ), A.interimAllocProb i z = B.interimAllocProb i z) (hM0 : A.interimExpectedPayment i 0 = B.interimExpectedPayment i 0) (v_i : ℝ) : A.interimExpectedPayment i v_i = B.interimExpectedPayment i v_i ∧ A.equilibriumPayoff i v_i = B.equilibriumPayoff i v_i

[MSZ 12.50] Same q_i and zero-type payment give the same interim objects.

def BayesianSingleItemAuction.HasNonnegativeInterimAllocationIntegralOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) : Prop

Nonnegative envelope increments on [0, ωᵢ].

Equations

• A.HasNonnegativeInterimAllocationIntegralOnSupport = ∀ (i : I) (v_i : ℝ), 0 ≤ v_i → v_i ≤ A.typeData.omega i → 0 ≤ ∫ (z : ℝ) in 0..v_i, A.interimAllocProb i z

theorem BayesianSingleItemAuction.hasNonnegativeInterimAllocationIntegralOnSupport_of_isFeasible {I : Type u_1} [Fintype I] (A : BayesianSingleItemAuction I) (hfeas : A.IsFeasible) : A.HasNonnegativeInterimAllocationIntegralOnSupport

Feasibility gives nonnegative envelope increments on the support.

theorem BayesianSingleItemAuction.isIndividuallyRationalOnSupport_iff_interimExpectedPayment_zero_nonpos {I : Type u_1} (A : BayesianSingleItemAuction I) (henv : A.HasInterimEnvelopeFormula) (hint_nonneg : A.HasNonnegativeInterimAllocationIntegralOnSupport) : A.IsIndividuallyRationalOnSupport ↔ ∀ (i : I), A.interimExpectedPayment i 0 ≤ 0

[MSZ 12.52] Supportwise IR iff zero-type payment is nonpositive.

theorem BayesianSingleItemAuction.interimExpectedPayment_zero_nonpos_of_isIndividuallyRationalOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (hIR : A.IsIndividuallyRationalOnSupport) (i : I) : A.interimExpectedPayment i 0 ≤ 0

Supportwise IR makes zero-type expected payment nonpositive.

theorem BayesianSingleItemAuction.interimExpectedPayment_le_alloc_mul_sub_integral_of_isIncentiveCompatible_of_isIndividuallyRationalOnSupport {I : Type u_1} (A : BayesianSingleItemAuction I) (hIC : A.IsIncentiveCompatible) (hIR : A.IsIndividuallyRationalOnSupport) (i : I) (v_i : ℝ) : A.interimExpectedPayment i v_i ≤ A.interimAllocProb i v_i * v_i - ∫ (z : ℝ) in 0..v_i, A.interimAllocProb i z

IC and IR bound interim expected payment by the envelope term.