Proof of `The energy-increment refinement lemma`
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
Every class is atomised simultaneously along the witnesses supplied by its irregular partners. A weighted variance calculation on each old pair gives the required global energy increment.