OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Grid.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryNarrowGrid.grid line 20
  2. def OAI.OrdinaryNarrowGrid.lower line 21
  3. def OAI.OrdinaryNarrowGrid.upper line 22
  4. lemma OAI.OrdinaryNarrowGrid.mesh_cover line 24
  5. lemma OAI.OrdinaryNarrowGrid.grid_cover line 37
  6. lemma OAI.OrdinaryNarrowGrid.grid_lower_pos line 54
  7. lemma OAI.OrdinaryNarrowGrid.lower_le_upper line 59
  8. lemma OAI.OrdinaryNarrowGrid.upper_le_two_lower line 63
  9. lemma OAI.OrdinaryNarrowGrid.upper_le_endpoint line 70
  10. lemma OAI.OrdinaryNarrowGrid.interval_disjoint_of_le line 81
  11. lemma OAI.OrdinaryNarrowGrid.grid_disjoint line 88
  12. lemma OAI.OrdinaryNarrowGrid.grid_card line 121
  13. lemma OAI.OrdinaryNarrowGrid.relative_width line 124