OAI/Combinatorics/KMedian/Expanders/SpectralWalk.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.PCP.expect_prod line 16
  2. def OAI.MetricKMedian.PCP.energy line 20
  3. def OAI.MetricKMedian.PCP.pairing line 21
  4. theorem OAI.MetricKMedian.PCP.energy_nonneg line 23
  5. theorem OAI.MetricKMedian.PCP.pairing_sq_le line 26
  6. theorem OAI.MetricKMedian.PCP.energy_center line 29
  7. theorem OAI.MetricKMedian.PCP.mean_center line 37
  8. theorem OAI.MetricKMedian.PCP.energy_indicator_le line 41
  9. def OAI.MetricKMedian.PCP.PortGraph.adjacency line 55
  10. theorem OAI.MetricKMedian.PCP.PortGraph.adjacency_const line 58
  11. theorem OAI.MetricKMedian.PCP.PortGraph.adjacency_add line 63
  12. theorem OAI.MetricKMedian.PCP.PortGraph.adjacency_sub line 69
  13. theorem OAI.MetricKMedian.PCP.PortGraph.adjacency_mean line 74
  14. theorem OAI.MetricKMedian.PCP.PortGraph.adjacency_selfAdjoint line 84
  15. def OAI.MetricKMedian.PCP.PortGraph.Contracts line 96
  16. def OAI.MetricKMedian.PCP.PortGraph.propagate line 99
  17. theorem OAI.MetricKMedian.PCP.PortGraph.propagate_zero line 104
  18. theorem OAI.MetricKMedian.PCP.PortGraph.propagate_succ line 106
  19. theorem OAI.MetricKMedian.PCP.PortGraph.propagate_mean line 109
  20. theorem OAI.MetricKMedian.PCP.PortGraph.propagate_contract line 115
  21. theorem OAI.MetricKMedian.PCP.PortGraph.correlation_sq line 127
  22. theorem OAI.MetricKMedian.PCP.PortGraph.propagate_const line 137
  23. theorem OAI.MetricKMedian.PCP.PortGraph.propagate_sub line 143
  24. theorem OAI.MetricKMedian.PCP.PortGraph.centered_correlation line 149
  25. theorem OAI.MetricKMedian.PCP.PortGraph.bounded_correlation line 162