OAI/Combinatorics/KMedian/Expanders/WalkMoments.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.PCP.expect_word_succ line 14
  2. theorem OAI.MetricKMedian.PCP.mean_sq_le_support_energy line 20
  3. def OAI.MetricKMedian.PCP.PortGraph.edgeHit line 39
  4. def OAI.MetricKMedian.PCP.PortGraph.edgeMass line 43
  5. def OAI.MetricKMedian.PCP.PortGraph.badCount line 45
  6. def OAI.MetricKMedian.PCP.PortGraph.countMean line 49
  7. def OAI.MetricKMedian.PCP.PortGraph.countSquareMean line 51
  8. theorem OAI.MetricKMedian.PCP.PortGraph.edgeHit_sq line 54
  9. theorem OAI.MetricKMedian.PCP.PortGraph.edgeHit_bounds line 60
  10. theorem OAI.MetricKMedian.PCP.PortGraph.edgeMass_bounds line 66
  11. theorem OAI.MetricKMedian.PCP.PortGraph.edgeMass_mean line 71
  12. theorem OAI.MetricKMedian.PCP.PortGraph.badCount_cons line 76
  13. theorem OAI.MetricKMedian.PCP.PortGraph.countMean_zero line 81
  14. theorem OAI.MetricKMedian.PCP.PortGraph.countMean_succ line 86
  15. theorem OAI.MetricKMedian.PCP.PortGraph.countMean_mean line 94
  16. theorem OAI.MetricKMedian.PCP.PortGraph.countMean_sum line 104
  17. theorem OAI.MetricKMedian.PCP.PortGraph.edge_cross line 118
  18. theorem OAI.MetricKMedian.PCP.PortGraph.edge_future_le line 133
  19. theorem OAI.MetricKMedian.PCP.PortGraph.countSquareMean_succ line 155
  20. theorem OAI.MetricKMedian.PCP.PortGraph.countSquareMean_le line 174
  21. theorem OAI.MetricKMedian.PCP.PortGraph.witness_second_moment line 186