OAI/Combinatorics/KMedian/Expanders/PathCount.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.PortGraph.badCount_eq_sum line 17
2. def OAI.MetricKMedian.PCP.PortGraph.Walk.ithHit line 28
3. def OAI.MetricKMedian.PCP.PortGraph.Walk.hitCount line 30
4. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.ithHit_nonneg line 32
5. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.hitCount_eq line 38
6. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.hitCount_nonneg line 50
7. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.partial_hits_le line 53
8. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.prefix_hitCount_le line 67
9. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.hitCount_second_moment line 82