OAI/Combinatorics/SparsestCut/RoundedCharts.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.SourceCharts.u line 19
  2. def OAI.UniformSparsestCut.SourceCharts.lower line 20
  3. lemma OAI.UniformSparsestCut.SourceCharts.lower_pos line 22
  4. lemma OAI.UniformSparsestCut.SourceCharts.energy line 23
  5. def OAI.UniformSparsestCut.SourceCharts.B line 30
  6. lemma OAI.UniformSparsestCut.SourceCharts.B_left line 32
  7. lemma OAI.UniformSparsestCut.SourceCharts.u_norm line 35
  8. lemma OAI.UniformSparsestCut.SourceCharts.u_nonzero line 37
  9. lemma OAI.UniformSparsestCut.SourceCharts.u_nonparallel line 40
  10. lemma OAI.UniformSparsestCut.SourceCharts.u_pivot line 49
  11. lemma OAI.UniformSparsestCut.SourceCharts.B_column line 55
  12. lemma OAI.UniformSparsestCut.SourceCharts.B_norm line 62
  13. lemma OAI.UniformSparsestCut.SourceCharts.residual_norm line 64
  14. lemma OAI.UniformSparsestCut.HyperplaneCount.shattered_independent line 75
  15. lemma OAI.UniformSparsestCut.HyperplaneCount.vcDim_le line 108
  16. lemma OAI.UniformSparsestCut.HyperplaneCount.sign_patterns_bound line 116
  17. def OAI.UniformSparsestCut.RoundedCharts.cube line 133
  18. def OAI.UniformSparsestCut.RoundedCharts.regular line 135
  19. def OAI.UniformSparsestCut.RoundedCharts.integerLabel line 138
  20. def OAI.UniformSparsestCut.RoundedCharts.rounded line 141
  21. def OAI.UniformSparsestCut.RoundedCharts.Vertex line 144
  22. def OAI.UniformSparsestCut.RoundedCharts.coordinate line 147
  23. lemma OAI.UniformSparsestCut.RoundedCharts.cube_norm line 150
  24. lemma OAI.UniformSparsestCut.RoundedCharts.hyperplane_null line 165
  25. lemma OAI.UniformSparsestCut.RoundedCharts.ae_regular line 188
  26. lemma OAI.UniformSparsestCut.RoundedCharts.rounded_error_coordinate line 197
  27. lemma OAI.UniformSparsestCut.RoundedCharts.rounded_error line 207
  28. lemma OAI.UniformSparsestCut.RoundedCharts.integerLabel_bound line 223
  29. lemma OAI.UniformSparsestCut.RoundedCharts.vertex_finite line 241
  30. lemma OAI.UniformSparsestCut.RoundedCharts.representative line 261
  31. lemma OAI.UniformSparsestCut.SourceCharts.lower_ge_one line 277
  32. lemma OAI.UniformSparsestCut.SourceCharts.B_norm_le line 283
  33. lemma OAI.UniformSparsestCut.SourceCharts.rounded_B_error line 285
  34. lemma OAI.UniformSparsestCut.SourceCharts.rounded_residual_error line 292
  35. lemma OAI.UniformSparsestCut.SourceCharts.vertex_B_bound line 303
  36. lemma OAI.UniformSparsestCut.SourceCharts.vertex_residual_bound line 310