Proof of `Choosing a collision-free outcome with bounded total path length` (2nd statement)
groundedproofs/Lax263307Proofs/SamplingOutcomes.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
On the event that cost exceeds the threshold, multiply that threshold by the outcome probability and bound it by the weighted cost. Nonnegative cost controls the other outcomes. Sum and divide by the positive threshold.