Appendix, Proof of Proposition 3, p. 28 — q(θ) = γθ/(s+γk) when γ ≤ s/k and q(θ) = θ/(2k) when γ ≥ s/k

Proved

CustomerVoice.OLearn.qStar_cases

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

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

Under the standing assumptions, for each buyer type with preference $\theta\in\{\theta_H,\theta_L\}$ ,

q^*(\theta)=\begin{cases}\dfrac{\gamma\theta}{s+\gamma k}, & \gamma\le s/k,\\[2mm] \dfrac{\theta}{2k}, & \gamma\ge s/k.\end{cases}

The two regimes are the ones in which the seller's acceptance constraint binds or does not bind at the first-best design, and the proof of Proposition 3 treats them separately.

Preamble

import Mathlib
import Definitions.Def_CustomerVoice_OLearn_Setting

Formal statement

namespace CustomerVoice.OLearn

theorem qStar_cases (M : Model) (hM : M.Standing) (t : CustomerVoice.ALearn.BType) :
    (M.γ ≤ M.s / M.k → M.qStar (M.θ t) = M.γ * M.θ t / (M.s + M.γ * M.k)) ∧
    (M.s / M.k ≤ M.γ → M.qStar (M.θ t) = M.θ t / (2 * 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

Appendix, Proof of Proposition 3, p. 28 — q*(θ) = γθ/(s+γk) when γ ≤ s/k and q*(θ) = θ/(2k) when γ ≥ s/k

Appendix, Proof of Proposition 3, p. 28 — q(θ) = γθ/(s+γk) when γ ≤ s/k and q(θ) = θ/(2k) when γ ≥ s/k