OAI/Combinatorics/KMedian/Amplification/PoweringMean.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedian.PCP.Stopped.weight_pair line 13
  2. lemma OAI.MetricKMedian.PCP.Stopped.atom_expect line 20
  3. def OAI.MetricKMedian.PCP.PortGraph.Walk.cast line 35
  4. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.cast_rfl line 36
  5. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.cast_vertex line 37
  6. lemma OAI.MetricKMedian.PCP.PortGraph.Walk.cast_port line 39
  7. def OAI.MetricKMedian.PCP.PortCSP.diagHit line 48
  8. lemma OAI.MetricKMedian.PCP.PortCSP.diagHit_mean line 53
  9. def OAI.MetricKMedian.PCP.PortCSP.witness line 62
  10. def OAI.MetricKMedian.PCP.PortCSP.stoppedWitness line 66
  11. lemma OAI.MetricKMedian.PCP.PortCSP.stopped_diag_mean line 72
  12. theorem OAI.MetricKMedian.PCP.PortCSP.witness_mean_eq line 90
  13. theorem OAI.MetricKMedian.PCP.PortCSP.witness_mean_ge line 123