OAI/Combinatorics/SparsestCut/ContractionBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.KernelGeometry.κ line 16
  2. def OAI.UniformSparsestCut.KernelGeometry.L line 17
  3. lemma OAI.UniformSparsestCut.KernelGeometry.smooth line 18
  4. lemma OAI.UniformSparsestCut.KernelGeometry.compact line 20
  5. lemma OAI.UniformSparsestCut.KernelGeometry.nonneg line 22
  6. lemma OAI.UniformSparsestCut.KernelGeometry.integral_one line 24
  7. lemma OAI.UniformSparsestCut.KernelGeometry.integrable line 26
  8. lemma OAI.UniformSparsestCut.KernelGeometry.L_nonneg line 28
  9. lemma OAI.UniformSparsestCut.KernelGeometry.support_coord line 30
  10. lemma OAI.UniformSparsestCut.KernelGeometry.tsupport_coord line 34
  11. lemma OAI.UniformSparsestCut.KernelGeometry.shifted_mem line 37
  12. lemma OAI.UniformSparsestCut.KernelGeometry.derivative_shifted_mem line 43
  13. lemma OAI.UniformSparsestCut.KernelGeometry.norm_bound line 49
  14. lemma OAI.UniformSparsestCut.KernelGeometry.partial_integrable line 51
  15. lemma OAI.UniformSparsestCut.KernelGeometry.partial_integral line 56
  16. def OAI.UniformSparsestCut.SourceContraction.H line 70
  17. lemma OAI.UniformSparsestCut.SourceContraction.H_nonneg line 71
  18. def OAI.UniformSparsestCut.SourceContraction.weight line 72
  19. def OAI.UniformSparsestCut.SourceContraction.C line 73
  20. lemma OAI.UniformSparsestCut.SourceContraction.C_pos line 74
  21. lemma OAI.UniformSparsestCut.SourceContraction.weight_ge_one line 80
  22. lemma OAI.UniformSparsestCut.SourceContraction.scale_L line 85
  23. lemma OAI.UniformSparsestCut.SourceContraction.small line 87
  24. lemma OAI.UniformSparsestCut.SourceContraction.contraction_numeric line 111
  25. lemma OAI.UniformSparsestCut.SourceCharts.good_dual line 167