OAI/Geometry/UnitDistances/Blocks.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.GenericGrid.edges line 12
  2. lemma OAI.PlanarUnitDistances.GenericGrid.edges_card_le line 16
  3. lemma OAI.PlanarUnitDistances.GenericGrid.side_card_lower line 23
  4. theorem OAI.PlanarUnitDistances.GenericGrid.grid_card_lower line 48
  5. theorem OAI.PlanarUnitDistances.GenericGrid.eventually_exists_avoiding line 71
  6. theorem OAI.PlanarUnitDistances.GenericGrid.choose_countable line 83
  7. lemma OAI.UnitDistanceBlockAvoidance.coeff_sumAlgEquiv line 100
  8. lemma OAI.UnitDistanceBlockAvoidance.coeff_degree_le line 106
  9. lemma OAI.UnitDistanceBlockAvoidance.outer_degree_le line 119
  10. lemma OAI.UnitDistanceBlockAvoidance.map_degree_le line 137
  11. lemma OAI.UnitDistanceBlockAvoidance.eval_blocks line 144
  12. theorem OAI.UnitDistanceBlockAvoidance.two_block_zero_count line 153
  13. abbrev OAI.UnitDistanceBlockAvoidance.BlockVars line 210
  14. abbrev OAI.UnitDistanceBlockAvoidance.BlockTuples line 214
  15. instance OAI.UnitDistanceBlockAvoidance.blockTuplesFintype line 218
  16. lemma OAI.UnitDistanceBlockAvoidance.blockTuples_card line 224
  17. def OAI.UnitDistanceBlockAvoidance.blockEval line 234
  18. def OAI.UnitDistanceBlockAvoidance.zeroCap line 239
  19. lemma OAI.UnitDistanceBlockAvoidance.zeroCap_succ line 243
  20. theorem OAI.UnitDistanceBlockAvoidance.blocks_zero_count line 248
  21. def OAI.UnitDistanceBlockAvoidance.zeroSet line 290
  22. def OAI.UnitDistanceBlockAvoidance.maxZeros line 294
  23. lemma OAI.UnitDistanceBlockAvoidance.attainable_zeros_nonempty line 297
  24. lemma OAI.UnitDistanceBlockAvoidance.attainable_zeros_bdd line 303
  25. lemma OAI.UnitDistanceBlockAvoidance.zeroSet_card_le line 310
  26. lemma OAI.UnitDistanceBlockAvoidance.maxZeros_attained line 314
  27. lemma OAI.UnitDistanceBlockAvoidance.maxZeros_le line 318
  28. def OAI.UnitDistanceBlockAvoidance.tupleEquiv line 324
  29. def OAI.UnitDistanceBlockAvoidance.blockGrids line 333
  30. lemma OAI.UnitDistanceBlockAvoidance.blockGrids_card line 339
  31. lemma OAI.UnitDistanceBlockAvoidance.mem_blockGrids line 344
  32. def OAI.PlanarUnitDistances.GenericGrid.UniformBlocks line 357
  33. lemma OAI.PlanarUnitDistances.GenericGrid.zeroCap_upper line 361
  34. theorem OAI.PlanarUnitDistances.GenericGrid.polynomial_test_saving line 374
  35. def OAI.PlanarUnitDistances.GenericGrid.optionalCoordinates line 431
  36. theorem OAI.PlanarUnitDistances.GenericGrid.choose_polynomial_tests line 436
  37. lemma OAI.UnitDistances.UltraField.mvmap_zero_iff line 489
  38. lemma OAI.UnitDistances.UltraField.mvmap_eventually_ne_zero line 513
  39. lemma OAI.UnitDistances.UltraField.mvmap_totalDegree_le line 518
  40. lemma OAI.UnitDistances.UltraField.mvmap_eval line 525
  41. instance OAI.UnitDistanceBlockAvoidance.blockVars_countable line 539
  42. theorem OAI.PlanarUnitDistances.GenericGrid.exists_independent_grid line 550
  43. def OAI.UnitDistanceBlockAvoidance.varIndex line 603
  44. lemma OAI.UnitDistanceBlockAvoidance.varIndex_injective line 607
  45. lemma OAI.UnitDistanceBlockAvoidance.blockEval_varIndex line 625
  46. def OAI.PlanarUnitDistances.GenericGrid.leftCoords line 643
  47. def OAI.PlanarUnitDistances.GenericGrid.rightCoords line 649
  48. lemma OAI.PlanarUnitDistances.GenericGrid.independent_left_right line 655
  49. theorem OAI.PlanarUnitDistances.GenericGrid.exists_real_grid line 686