OAI/NumberTheory/GaussianMoat/BooleanCube.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.Cube line 11
  2. instance OAI.GaussianMoat.cubeFintype line 14
  3. instance OAI.GaussianMoat.cubeDecidableEq line 17
  4. def OAI.GaussianMoat.cubeDist line 20
  5. theorem OAI.GaussianMoat.cubeDist_self line 23
  6. theorem OAI.GaussianMoat.cubeDist_zero_iff line 27
  7. theorem OAI.GaussianMoat.cubeDist_symm line 34
  8. theorem OAI.GaussianMoat.cubeDist_triangle line 41
  9. def OAI.GaussianMoat.cubeSize line 52
  10. def OAI.GaussianMoat.cubeBoundary line 55
  11. def OAI.GaussianMoat.cubeCross line 58
  12. theorem OAI.GaussianMoat.cubeSize_succ line 62
  13. theorem OAI.GaussianMoat.cubeBoundary_succ line 68
  14. theorem OAI.GaussianMoat.cubeCross_card_le line 79
  15. theorem OAI.GaussianMoat.cube_degree line 86
  16. theorem OAI.GaussianMoat.binEntropy_ge_two_mul line 97
  17. theorem OAI.GaussianMoat.entropy_merge_of_le line 106
  18. theorem OAI.GaussianMoat.entropy_merge line 128
  19. theorem OAI.GaussianMoat.cube_edge_isoperimetric line 138
  20. def OAI.GaussianMoat.cubeExpand line 169
  21. def OAI.GaussianMoat.cubeExpandIter line 172
  22. theorem OAI.GaussianMoat.cubeSize_mono line 176
  23. theorem OAI.GaussianMoat.cube_card line 185
  24. theorem OAI.GaussianMoat.cubeSize_le line 193
  25. theorem OAI.GaussianMoat.cubeBoundary_expand_bound line 202
  26. theorem OAI.GaussianMoat.cubeExpandIter_witness line 237
  27. theorem OAI.GaussianMoat.cubeExpandIter_disjoint line 248
  28. theorem OAI.GaussianMoat.cubeSize_sum_le line 259
  29. theorem OAI.GaussianMoat.cube_growth line 281
  30. theorem OAI.GaussianMoat.cube_iter_growth line 300
  31. theorem OAI.GaussianMoat.cube_separated_bound line 324