OAI/Combinatorics/SparsestCut/CubePoincare.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformSparsestCut.CubePoincare.Ψ line 16
  2. def OAI.UniformSparsestCut.CubePoincare.cube line 17
  3. instance OAI.UniformSparsestCut.CubePoincare.cube_probability line 19
  4. def OAI.UniformSparsestCut.CubePoincare.coordinate line 23
  5. lemma OAI.UniformSparsestCut.CubePoincare.coordinate_apply line 26
  6. def OAI.UniformSparsestCut.CubePoincare.derivative line 28
  7. lemma OAI.UniformSparsestCut.CubePoincare.derivative_apply line 32
  8. lemma OAI.UniformSparsestCut.CubePoincare.Ψ_hasFDeriv line 34
  9. lemma OAI.UniformSparsestCut.CubePoincare.Ψ_contDiff line 40
  10. lemma OAI.UniformSparsestCut.CubePoincare.Ψ_norm line 45
  11. lemma OAI.UniformSparsestCut.CubePoincare.derivative_norm line 59
  12. lemma OAI.UniformSparsestCut.CubePoincare.Ψ_map line 76
  13. lemma OAI.UniformSparsestCut.CubePoincare.cube_first_moment line 88