OAI/Combinatorics/SparsestCut/Directions.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniformSparsestCut.Directions.integral_eval line 19
  2. lemma OAI.UniformSparsestCut.Directions.real_measure_eval line 27
  3. lemma OAI.UniformSparsestCut.Directions.iid_bounded_concentration line 32
  4. lemma OAI.UniformSparsestCut.Directions.real_measure_exists_le line 52
  5. def OAI.UniformSparsestCut.Directions.badCount line 64
  6. lemma OAI.UniformSparsestCut.Directions.bad_chart_fraction line 68
  7. lemma OAI.UniformSparsestCut.Directions.exists_outside_of_real_lt_one line 103
  8. lemma OAI.UniformSparsestCut.Directions.exists_outside_with_ae line 111
  9. lemma OAI.UniformSparsestCut.Directions.finite_union_bound line 123
  10. def OAI.UniformSparsestCut.Directions.fourierSummand line 140
  11. def OAI.UniformSparsestCut.Directions.covarianceSummand line 142
  12. def OAI.UniformSparsestCut.Directions.normBad line 145
  13. def OAI.UniformSparsestCut.Directions.fourierBad line 147
  14. def OAI.UniformSparsestCut.Directions.covarianceBad line 149
  15. def OAI.UniformSparsestCut.Directions.projectionBad line 151
  16. lemma OAI.UniformSparsestCut.Directions.fourierSummand_measurable line 154
  17. lemma OAI.UniformSparsestCut.Directions.covarianceSummand_measurable line 157
  18. lemma OAI.UniformSparsestCut.Directions.normBad_measurable line 159
  19. lemma OAI.UniformSparsestCut.Directions.fourierBad_measurable line 161
  20. lemma OAI.UniformSparsestCut.Directions.covarianceBad_measurable line 166
  21. lemma OAI.UniformSparsestCut.Directions.projectionBad_measurable line 171
  22. lemma OAI.UniformSparsestCut.Directions.normBad_bound line 174
  23. lemma OAI.UniformSparsestCut.Directions.fourierBad_bound line 185
  24. lemma OAI.UniformSparsestCut.Directions.covarianceBad_bound line 191
  25. lemma OAI.UniformSparsestCut.Directions.projectionBad_bound line 196
  26. def OAI.UniformSparsestCut.Directions.chartBad line 201
  27. lemma OAI.UniformSparsestCut.Directions.chartBad_measurable line 205
  28. lemma OAI.UniformSparsestCut.Directions.chartBad_bound line 218
  29. lemma OAI.UniformSparsestCut.Directions.projection_chart_fraction line 232
  30. lemma OAI.UniformSparsestCut.Directions.goodBad_bound line 241
  31. theorem OAI.UniformSparsestCut.Directions.select_on_nets line 251