OAI/Probability/LatticeSurface/Coercivity/GridTraceGeometry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GridTrace.NatGrid.lo line 20
  2. def OAI.GridTrace.NatGrid.hi line 22
  3. def OAI.GridTrace.NatGrid.box line 24
  4. def OAI.GridTrace.NatGrid.square line 26
  5. abbrev OAI.GridTrace.NatGrid.Edge line 28
  6. def OAI.GridTrace.NatGrid.edges line 30
  7. def OAI.GridTrace.NatGrid.edgeGrad line 34
  8. def OAI.GridTrace.NatGrid.anchor line 38
  9. lemma OAI.GridTrace.NatGrid.square_mem line 42
  10. lemma OAI.GridTrace.NatGrid.mem_box_iff line 45
  11. lemma OAI.GridTrace.NatGrid.box_self line 51
  12. lemma OAI.GridTrace.NatGrid.box_subset line 56
  13. lemma OAI.GridTrace.NatGrid.box_subset_square line 61
  14. lemma OAI.GridTrace.NatGrid.box_zero line 65
  15. lemma OAI.GridTrace.NatGrid.box_full line 74
  16. lemma OAI.GridTrace.NatGrid.side_lower line 81
  17. lemma OAI.GridTrace.NatGrid.side_upper line 86
  18. lemma OAI.GridTrace.NatGrid.box_card_lower line 91
  19. lemma OAI.GridTrace.NatGrid.edges_sum line 96
  20. lemma OAI.GridTrace.NatGrid.edges_subset line 100
  21. lemma OAI.GridTrace.NatGrid.box_edges_subset line 111
  22. lemma OAI.GridTrace.NatGrid.anchor_mem_rect line 115
  23. lemma OAI.GridTrace.NatGrid.edges_card_bound line 124
  24. lemma OAI.GridTrace.NatGrid.dyadic_step line 135