Prove2Me

Appendix, Proof of Proposition 3, p. 28 — ΛH1 ≤ ΛH2 if and only if γ ≤ s/k

Proved
CustomerVoice.OLearn.lambdaH1_le_lambdaH2_iff

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

customizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Under the standing assumptions,

ΛH1=γ(s+k)(1−γ)s ≤ ΛH2=1+γ1−γ  ⟺  γ≤sk.\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s}\ \le\ \Lambda_{H2}=\frac{1+\gamma}{1-\gamma}\iff \gamma\le \frac{s}{k}.

This identifies which of the two high-type thresholds enters Λ=max⁡{min⁡{ΛH1,ΛH2},ΛL}\Lambda=\max\{\min\{\Lambda_{H1},\Lambda_{H2}\},\Lambda_L\} in each regime, and closes the proof of Proposition 3.

Preamble
import Mathlib
import Definitions.Def_CustomerVoice_OLearn_Setting
Formal statement
namespace CustomerVoice.OLearn

theorem lambdaH1_le_lambdaH2_iff (M : Model) (hM : M.Standing) :
    M.LambdaH1 ≤ M.LambdaH2 ↔ M.γ ≤ M.s / M.k := by sorry

end CustomerVoice.OLearn
Source
Guo, The Voice of Customers in Customization, SSRN working paper 3994319 (version of 2023-11-29, https://ssrn.com/abstract=3994319), p. 28, Appendix, Proof of Proposition 3
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