Prove2Me

Proof of Lemma 5, p. 33 — q₂(c) < q₁(c) (for β < 1) and q₁(c) < 1

Proved
NewsBundling.Negotiated.q2_lt_q1_and_q1_lt_one

by mikedeng1 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

content-bundlingnash-bargainingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Assume 13<β≤1\tfrac13<\beta\le1, c>2βc>2\beta and 0<Λ<120<\Lambda<\tfrac12, and let q1(c)=(1+β)/(2c)q_1(c)=(1+\beta)/(2c) and q2(c)=(β(2−Λ)−Λ)/(2(1−Λ)c)q_2(c)=(\beta(2-\Lambda)-\Lambda)/(2(1-\Lambda)c). Then

q1(c)<1,and, if β<1,q2(c)<q1(c).q_1(c)<1,\qquad\text{and, if }\beta<1,\qquad q_2(c)<q_1(c).

These inequalities place the equilibrium quality of Lemma 5 inside [0,1][0,1] and order the two thresholds of Lemma 5.

Formalization Note The paper states q2(c)<q1(c)q_2(c)<q_1(c) "for all cc". At β=1\beta=1 the two coincide (q1=q2=1/cq_1=q_2=1/c), so the strict inequality is stated under β<1\beta<1.

Preamble
import Mathlib
import Definitions.Def_NewsBundling_Negotiated_Setting
Formal statement
namespace NewsBundling.Negotiated

theorem q2_lt_q1_and_q1_lt_one (β c Λ : ℝ) (hN : NegAssumptions β c Λ) :
    (β < 1 → q2 β c Λ < q1 β c) ∧ q1 β c < 1 := by sorry

end NewsBundling.Negotiated
Source
de Cornière & Sarvary, Social Media and News: Content Bundling and News Quality, TSE Working Paper n° 1152 (August 2021), App. A, proof of Lemma 5, p. 33, last paragraph (and p. 32, first sentence)
Human review

  • Endorsed by Shuze Chen · Oct 16, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 16, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph