OAI/Combinatorics/KMedian/Expanders/Stopped.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.Stopped.length line 15
  2. theorem OAI.MetricKMedian.PCP.Stopped.length_le line 19
  3. theorem OAI.MetricKMedian.PCP.Stopped.length_cons line 28
  4. def OAI.MetricKMedian.PCP.Stopped.survival line 32
  5. def OAI.MetricKMedian.PCP.Stopped.stopping line 33
  6. theorem OAI.MetricKMedian.PCP.Stopped.survival_nonneg line 35
  7. theorem OAI.MetricKMedian.PCP.Stopped.stopping_nonneg line 36
  8. theorem OAI.MetricKMedian.PCP.Stopped.survival_add_stopping line 37
  9. theorem OAI.MetricKMedian.PCP.Stopped.coin_expect line 42
  10. theorem OAI.MetricKMedian.PCP.Stopped.expectation line 51
  11. theorem OAI.MetricKMedian.PCP.Stopped.weights_sum line 76
  12. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.prefix_expect line 86
  13. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.prefix_expect_le line 94
  14. theorem OAI.MetricKMedian.PCP.PortGraph.Walk.stopped_expect line 99