OAI/Combinatorics/KMedian/Expanders/Cloud.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.PCP.PortGraph.average line 17
  2. def OAI.MetricKMedian.PCP.PortGraph.lift line 18
  3. def OAI.MetricKMedian.PCP.PortGraph.residual line 19
  4. lemma OAI.MetricKMedian.PCP.PortGraph.lift_energy line 21
  5. lemma OAI.MetricKMedian.PCP.PortGraph.lift_l2 line 26
  6. lemma OAI.MetricKMedian.PCP.PortGraph.average_mean line 29
  7. lemma OAI.MetricKMedian.PCP.PortGraph.average_energy line 32
  8. lemma OAI.MetricKMedian.PCP.PortGraph.residual_mean line 40
  9. lemma OAI.MetricKMedian.PCP.PortGraph.residual_energy line 45
  10. lemma OAI.MetricKMedian.PCP.PortGraph.residual_energy_le line 53
  11. lemma OAI.MetricKMedian.PCP.PortGraph.average_l2 line 57
  12. lemma OAI.MetricKMedian.PCP.PortGraph.residual_l2 line 59
  13. lemma OAI.MetricKMedian.PCP.PortGraph.decompose line 63
  14. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_add line 69
  15. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_lift line 76
  16. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_decompose line 82
  17. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_residual_energy line 89
  18. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_residual_l2 line 98
  19. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_energy_le line 103
  20. lemma OAI.MetricKMedian.PCP.PortGraph.cloud_l2_le line 111
  21. lemma OAI.MetricKMedian.PCP.PortGraph.permute_add line 115
  22. lemma OAI.MetricKMedian.PCP.PortGraph.permute_energy line 119
  23. lemma OAI.MetricKMedian.PCP.PortGraph.permute_l2 line 124
  24. lemma OAI.MetricKMedian.PCP.PortGraph.average_permute_lift line 129