Prove2Me

Lemma 3, p. 36 — for π ∈ Π_AP and k > q: λ_H^{k−q} π_q ≤ π_k ≤ λ^{k−q} π_q; π_k ∈ (0, 1) when λ_H > 0

Proved
NeedPersuasion.FullInfo.lemma_3

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

information-designp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1queueing

Assume the standing assumptions of the model and let π∈ΠAP\pi\in\Pi_{AP} be an admission policy. Then for all k>qk>q in N0\mathbb N_0,

λH k−q πq  ≤  πk  ≤  λk−q πq.\lambda_H^{\,k-q}\,\pi_q\;\le\;\pi_k\;\le\;\lambda^{k-q}\,\pi_q .

In particular, if λH>0\lambda_H>0, then 0<πk<10<\pi_k<1 for every k∈N0k\in\mathbb N_0.

The two-sided geometric sandwich follows the detailed-balance constraints step by step; it is the basic comparison tool behind every perturbation and stochastic-dominance argument of the paper.

Preamble
import Mathlib
import Definitions.Def_NeedPersuasion_FullInfo_Model
Formal statement
namespace NeedPersuasion.FullInfo

theorem lemma_3 (M : Model) (hM : M.Standing) (π : ℕ → ℝ) (hπ : π ∈ PiAP M) :
    (∀ q k : ℕ, q < k → M.lamH ^ (k - q) * π q ≤ π k ∧ π k ≤ M.lam ^ (k - q) * π q) ∧
      (0 < M.lamH → ∀ k : ℕ, 0 < π k ∧ π k < 1) := by sorry

end NeedPersuasion.FullInfo
Source
arXiv:2005.07253v3, Lemma 3, p. 36
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