OAI/Combinatorics/KMedian/Process/ForceBatchBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.PhysicalPotential.time_increase_le line 15
2. def OAI.MetricKMedian.FixedBatch.nextAliveAt line 32
3. theorem OAI.MetricKMedian.FixedBatch.nextAliveAt_subset line 38
4. theorem OAI.MetricKMedian.FixedBatch.nextAliveAt_zero line 45
5. theorem OAI.MetricKMedian.FixedBatch.changeAt_probability_le line 53
6. theorem OAI.MetricKMedian.FixedBatch.post_force_bound line 70