Proof of `Infinity-distance projection LP and its separating dual` (1st statement)
groundedproofs/Lax263307Proofs/DistanceProjection.lean · lax-263307
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The distance column bounds the sum of the two nonnegative multiplier families by one. Their difference is therefore bounded in L1, and the original columns and rows make it valid on every feasible point.