OAI/NumberTheory/GaussianMoat/WalkGeometry.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianMoat.colorEdge line 10
  2. def OAI.GaussianMoat.Tricolored line 13
  3. theorem OAI.GaussianMoat.colorEdge_add line 15
  4. theorem OAI.GaussianMoat.colorEdge_zero_left line 21
  5. theorem OAI.GaussianMoat.colorEdge_zero_one line 24
  6. theorem OAI.GaussianMoat.colorEdge_binary line 27
  7. theorem OAI.GaussianMoat.discrete_rectangle_sperner line 32
  8. def OAI.GaussianMoat.pointColor line 86
  9. theorem OAI.GaussianMoat.pointColor_zero line 88
  10. theorem OAI.GaussianMoat.pointColor_one line 95
  11. theorem OAI.GaussianMoat.pointColor_two line 102
  12. theorem OAI.GaussianMoat.tricolored_covers line 109
  13. theorem OAI.GaussianMoat.tricolored_norm_bound line 115
  14. theorem OAI.GaussianMoat.discrete_rectangle_approx_zero line 146
  15. def OAI.GaussianMoat.repeatPath line 181
  16. theorem OAI.GaussianMoat.repeatPath_zero line 184
  17. theorem OAI.GaussianMoat.repeatPath_multiple line 187
  18. theorem OAI.GaussianMoat.repeatPath_step line 190
  19. theorem OAI.GaussianMoat.discrete_rectangle_approx_zero_rev line 210
  20. theorem OAI.GaussianMoat.path_difference_cover line 235
  21. theorem OAI.GaussianMoat.path_difference_cover_horizontal line 317
  22. theorem OAI.GaussianMoat.path_difference_cover_general line 341
  23. def OAI.GaussianMoat.latticeCoords line 372
  24. def OAI.GaussianMoat.latticeBasis line 382
  25. instance OAI.GaussianMoat.(instance at line 385) line 385
  26. instance OAI.GaussianMoat.(instance at line 386) line 386
  27. def OAI.GaussianMoat.twoVectorMap line 388
  28. theorem OAI.GaussianMoat.twoVectorMap_apply line 391
  29. theorem OAI.GaussianMoat.twoVectorMap_det line 400
  30. theorem OAI.GaussianMoat.twoVectorMap_injective line 405
  31. theorem OAI.GaussianMoat.twoVectorMap_quotient_card line 418
  32. def OAI.GaussianMoat.latticeBall line 429
  33. theorem OAI.GaussianMoat.mem_latticeBall line 432
  34. theorem OAI.GaussianMoat.complex_div_im_ne_zero line 435
  35. theorem OAI.GaussianMoat.lattice_path_difference_cover line 448
  36. theorem OAI.GaussianMoat.lattice_path_difference_card line 463
  37. theorem OAI.GaussianMoat.lattice_norm_ge_one line 503
  38. theorem OAI.GaussianMoat.lattice_dist_ge_one line 509
  39. def OAI.GaussianMoat.latticePixel line 513
  40. theorem OAI.GaussianMoat.abs_sub_lt_half_of_pixel_eq line 516
  41. theorem OAI.GaussianMoat.latticePixel_injective line 524
  42. theorem OAI.GaussianMoat.lattice_rectangle_card line 540