OAI/Combinatorics/KMedian/Expanders/L2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.l2 line 15
  2. lemma OAI.MetricKMedian.PCP.l2_nonneg line 16
  3. lemma OAI.MetricKMedian.PCP.l2_sq line 17
  4. lemma OAI.MetricKMedian.PCP.pairing_le_l2 line 19
  5. lemma OAI.MetricKMedian.PCP.energy_add line 27
  6. lemma OAI.MetricKMedian.PCP.l2_add line 34
  7. lemma OAI.MetricKMedian.PCP.l2_le_of_energy_le line 43
  8. lemma OAI.MetricKMedian.PCP.l2_mono line 49
  9. lemma OAI.MetricKMedian.PCP.mean_sq_le_energy line 52
  10. lemma OAI.MetricKMedian.PCP.PortGraph.energy_adjacency_le line 62
  11. lemma OAI.MetricKMedian.PCP.PortGraph.l2_adjacency_le line 69
  12. lemma OAI.MetricKMedian.PCP.PortGraph.l2_contracts line 72