Proposition 1(b) — without contracting the retailer shares no information
ProvedInfoSharing.Diseconomy.prop_1b_no_free_sharinginformation-sharingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain
Under the hypotheses of Lemma 3, suppose the retailer chooses the information statuses freely, with no side payment. Then a retailer-optimal status profile exists, and every retailer-optimal profile has
This is the benchmark that motivates the paid contracting of §5.2.
Formalization Note. The pricing stage is the Bayesian game of §4.1 on the signal model; the ex ante profits , are those of an arbitrary pricing-equilibrium family, not the §4.2 closed forms. Wholesale strategies are measurable, square-integrable functions of the signal value (constants for an uninformed manufacturer); the production cost is with and ; manufacturers are indexed by .
Preamble
import Mathlib import Definitions.Def_InfoSharing_Shared_IsSignalModel import Definitions.Def_InfoSharing_Shared_PayoffTable open MeasureTheory open InfoSharing.Shared
Formal statement
namespace InfoSharing.Diseconomy
/-- Proposition 1(b), p. 253: without information contracting, the retailer does not share any
information — a retailer-optimal status profile exists, and every one has no informed
manufacturer. -/
theorem prop_1b_no_free_sharing {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
(θ Y : Ω → ℝ) (a b c φ σ β : ℝ) (hmodel : IsSignalModel μ θ Y σ β) (hφ : 0 < φ)
(hb : 0 < b) (hc : 0 < c) (E : (Fin 2 → Status) → PricingProfile)
(hE : IsPricingEqFamily μ θ Y a b c φ β E) :
let P := payoffTable μ θ Y a b c φ E
(∃ X : Fin 2 → Status, IsNoContractOutcome P X) ∧
∀ X : Fin 2 → Status, IsNoContractOutcome P X → numInformed X = 0 := by sorry
end InfoSharing.Diseconomy
Source
Shang, Ha & Tong, Information Sharing in a Supply Chain with a Common Retailer, Management Sci. 62(1) 2016, p. 253, Proposition 1(b)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.