Proof of `Quantitative trimming after restrictions of a leaf mixture` (4th statement)
groundedproofs/Lax342547Proofs/LeafTrimming.lean · lax-342547
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
First compare the restricted mixed law pointwise to the original law, then push this comparison through the projection. The original marginal cap is charged only the actual mixed-law normalization cost.