OAI/MathematicalPhysics/Heisenberg/LatticeCuts.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Geometry.Ball line 10
  2. lemma OAI.Heisenberg.Geometry.step_translate line 13
  3. lemma OAI.Heisenberg.Geometry.reach_translate line 24
  4. lemma OAI.Heisenberg.Geometry.translate_mem_ball line 32
  5. def OAI.Heisenberg.Geometry.ballFinset line 36
  6. lemma OAI.Heisenberg.Geometry.mem_ballFinset line 39
  7. lemma OAI.Heisenberg.Geometry.ballFinset_card line 50
  8. theorem OAI.Heisenberg.Geometry.local_connectivity line 54
  9. def OAI.Heisenberg.LatticePotential.integral line 108
  10. lemma OAI.Heisenberg.LatticePotential.integral_zero line 112
  11. lemma OAI.Heisenberg.LatticePotential.integral_succ line 114
  12. lemma OAI.Heisenberg.LatticePotential.integral_ext_zero line 130
  13. lemma OAI.Heisenberg.LatticePotential.integral_sub line 142
  14. lemma OAI.Heisenberg.LatticePotential.integral_telescoping line 146
  15. abbrev OAI.Heisenberg.LatticePotential.Site line 152
  16. def OAI.Heisenberg.LatticePotential.shift line 154
  17. lemma OAI.Heisenberg.LatticePotential.shift_cons_zero line 156
  18. lemma OAI.Heisenberg.LatticePotential.shift_cons_succ line 161
  19. def OAI.Heisenberg.LatticePotential.Closed line 170
  20. theorem OAI.Heisenberg.LatticePotential.exists_potential line 173
  21. abbrev OAI.Heisenberg.LatticeCut.Edge line 219
  22. def OAI.Heisenberg.LatticeCut.color line 221
  23. def OAI.Heisenberg.LatticeCut.Cut line 223
  24. def OAI.Heisenberg.LatticeCut.square line 225
  25. def OAI.Heisenberg.LatticeCut.Linked line 228
  26. def OAI.Heisenberg.LatticeCut.CutReach line 231
  27. lemma OAI.Heisenberg.LatticeCut.cutReach_cut line 233
  28. lemma OAI.Heisenberg.LatticeCut.cutReach_square line 238
  29. def OAI.Heisenberg.LatticeCut.gradient line 243
  30. lemma OAI.Heisenberg.LatticeCut.shift_comm line 246
  31. lemma OAI.Heisenberg.LatticeCut.gradient_closed line 256
  32. def OAI.Heisenberg.LatticeCut.Connected line 284
  33. lemma OAI.Heisenberg.LatticeCut.step_shift line 287
  34. lemma OAI.Heisenberg.LatticeCut.potential_constant line 304
  35. theorem OAI.Heisenberg.LatticeCut.cut_connected line 322