Proof of `Monotonicity of partition energy under refinement`
groundedproofs/Lax18Proofs/PartitionEnergyMonotonicity.lean · lax-18
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 density on each coarse pair is the weighted average of the densities on the fine pairs above it. Finite Cauchy–Schwarz on every fibre, followed by summation, proves that refinement cannot decrease partition energy.