Prove2Me

p. 14 — α₁(x) ≤ α₂(x) for all x ∈ (0, 1)

Proved
GDPRPrivacy.PriceRise.alpha1_le_alpha2

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

gdprp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1pricingprivacythreshold

For every opt-in benefit 0<x<10 < x < 1,

α1(x)=max⁡{1−2x2,0}  ≤  α2(x)=max⁡{2−4x+x22x,0}.\alpha_1(x) = \max\Big\{\frac{1 - 2x}{2}, 0\Big\} \;\le\; \alpha_2(x) = \max\Big\{\frac{2 - 4x + x^2}{2x}, 0\Big\}.

The pre-GDPR threshold separating cases 1a and 1b never exceeds the post-GDPR threshold separating cases 2a and 2b. Hence a case 1a equilibrium before the GDPR never coexists with a case 2b equilibrium after it, which leaves exactly three possible pairs of equilibria (Lemma A3).

Preamble
import Mathlib
import Definitions.Def_GDPRPrivacy_PriceRise_Model
Formal statement
namespace GDPRPrivacy.PriceRise

theorem alpha1_le_alpha2 (x : ℝ) (hx0 : 0 < x) (hx1 : x < 1) :
    alpha1 x ≤ alpha2 x := by sorry

end GDPRPrivacy.PriceRise
Source
Choe, Matsushima & Shekhar, The Bright Side of the GDPR, ISER DP No. 1246 (June 2024), p. 14 ("one can verify that α₁(x) ≤ α₂(x) for all x ∈ (0, 1)"); restated p. 33
Human review

  • Endorsed by Shuze Chen · Oct 14, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 14, 2026

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

View graph