Prove2Me

Proof of Proposition 3, ec13 — algebraic maximum equals 4η/(1−η)²

Proved
CarlssonPartition.Approx.max_identity

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

heavy-trafficp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1region-partitioningvehicle-routing

For a real error factor 0≤η<10\le\eta<1, the larger of the relative upper and lower deviations is the upper deviation, and it simplifies to

max⁡{(1+η1−η)2−1,  1−(1−η1+η)2}=(1+η1−η)2−1=4η(1−η)2.\max\left\{\left(\frac{1+\eta}{1-\eta}\right)^2-1,\; 1-\left(\frac{1-\eta}{1+\eta}\right)^2\right\} =\left(\frac{1+\eta}{1-\eta}\right)^2-1 =\frac{4\eta}{(1-\eta)^2}.

This real algebra identity converts the two district comparisons into the paper's absolute error factor.

Formalization Note The hypothesis 0≤η<10\le\eta<1 is the sign range used in the Proposition 3 proof; this item states only the algebraic part of its last display.

Preamble
import Mathlib
import Definitions.Def_CarlssonPartition_Approx_Setting
Formal statement
namespace CarlssonPartition.Approx

theorem max_identity (η : ℝ) (hη0 : 0 ≤ η) (hη1 : η < 1) :
    max (((1 + η) / (1 - η)) ^ 2 - 1)
        (1 - ((1 - η) / (1 + η)) ^ 2) =
      ((1 + η) / (1 - η)) ^ 2 - 1 ∧
    ((1 + η) / (1 - η)) ^ 2 - 1 = 4 * η / (1 - η) ^ 2 := by sorry
end CarlssonPartition.Approx
Source
Carlsson, Liu, Salari and Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, accepted manuscript (SSRN 3915544; published in Operations Research 72(1):91–109, 2024, doi:10.1287/opre.2021.0588), proof of Proposition 3, p. ec13 (PDF 50), final display
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