OAI/Combinatorics/Progressions/Sampling/BoundedKernelGridEnumerationBudget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_card_real_grid_box line 9

    Distinct definitions of this name: OAI/Combinatorics/Progressions/Sampling/NativeGridRightDictionary.lean:9 (different declaration text). Qualify references as OAI.Erdos3.finite_card_real_grid_box@path.

  2. theorem OAI.Erdos3.real_grid_shifted_integer_bound line 49
  3. theorem OAI.Erdos3.finite_card_real_grid_window line 67
  4. theorem OAI.Erdos3.exists_real_grid_window_enumeration line 102
  5. theorem OAI.Erdos3.exists_scalar_rational_grid_window line 129
  6. theorem OAI.Erdos3.real_grid_window_count_le_exp line 172
  7. theorem OAI.Erdos3.exists_real_grid_window_enumeration_exp line 197
  8. theorem OAI.Erdos3.exists_uniform_real_grid_window_enumeration line 210
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_bounded_kernel_grid_enumeration line 246
  10. theorem OAI.Erdos3.real_grid_integer_box_count_bound line 296
  11. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_bounded_kernel_grid_enumeration_exp line 328
  12. theorem OAI.Erdos3.NilpotentLieBCHGroup.exists_uniform_bounded_kernel_grid_enumeration line 345