OAI/Combinatorics/Progressions/Sampling/RationalInactiveGridIntegralComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rationalInactive_partial_grid_conditional line 49
  2. theorem OAI.Erdos3.rationalInactive_partial_reference_conditional line 59
  3. theorem OAI.Erdos3.rationalInactive_partial_grid_integrable line 66
  4. theorem OAI.Erdos3.rationalInactive_partial_reference_integrable line 76
  5. theorem OAI.Erdos3.rationalInactive_partial_reference_integral line 85
  6. theorem OAI.Erdos3.rationalInactive_partial_grid_sub_reference_integral line 102
  7. theorem OAI.Erdos3.rationalInactive_translated_grid_comparison line 123
  8. theorem OAI.Erdos3.rationalInactive_partial_grid_integral_norm_comparison line 183
  9. theorem OAI.Erdos3.rationalInactive_partial_grid_comparison line 266