OAI/Combinatorics/SparsestCut/TriangleRepair.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniformSparsestCut.TriangleRepair.exp_distance_intervalIntegrable line 14
  2. lemma OAI.UniformSparsestCut.TriangleRepair.min_posSemidef line 23
  3. lemma OAI.UniformSparsestCut.TriangleRepair.abs_sub_sq_hilbert line 59
  4. lemma OAI.UniformSparsestCut.TriangleRepair.l1_sq_hilbert line 78
  5. lemma OAI.UniformSparsestCut.TriangleRepair.repair_integral_le line 97
  6. lemma OAI.UniformSparsestCut.TriangleRepair.repair_integral_local line 106
  7. def OAI.UniformSparsestCut.TriangleRepair.chartKernel line 136
  8. def OAI.UniformSparsestCut.TriangleRepair.cappedDistance line 139
  9. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_posSemidef line 143
  10. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_intervalIntegrable line 158
  11. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_nonneg line 167
  12. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_le_one line 173
  13. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_self line 182
  14. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_symm line 186
  15. lemma OAI.UniformSparsestCut.TriangleRepair.cappedDistance_nonneg line 192
  16. lemma OAI.UniformSparsestCut.TriangleRepair.cappedDistance_le line 200
  17. def OAI.UniformSparsestCut.TriangleRepair.ChartTriangle line 207
  18. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_mul_le line 212
  19. lemma OAI.UniformSparsestCut.TriangleRepair.chartKernel_le_half line 231
  20. def OAI.UniformSparsestCut.TriangleRepair.IsRepairGram line 251
  21. lemma OAI.UniformSparsestCut.TriangleRepair.exists_repairGram line 256
  22. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_norm_sq line 264
  23. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_distance line 272
  24. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_distance_le line 282
  25. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_local line 296
  26. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_eq_of_zero line 307
  27. def OAI.UniformSparsestCut.TriangleRepair.angleIntegrand line 315
  28. lemma OAI.UniformSparsestCut.TriangleRepair.angleIntegrand_integrable line 319
  29. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_angle line 325
  30. lemma OAI.UniformSparsestCut.TriangleRepair.angleIntegrand_nonneg line 345
  31. lemma OAI.UniformSparsestCut.TriangleRepair.angleIntegrand_ge_quarter line 355
  32. lemma OAI.UniformSparsestCut.TriangleRepair.repairGram_angle_lower line 371
  33. lemma OAI.UniformSparsestCut.TriangleRepair.chart_l1_sq_hilbert line 400
  34. lemma OAI.UniformSparsestCut.TriangleRepair.sum_sq_hilbert line 419
  35. lemma OAI.UniformSparsestCut.TriangleRepair.angle_triangle_slack line 429
  36. theorem OAI.UniformSparsestCut.TriangleRepair.triangle_repair line 437