OAI/Combinatorics/Progressions/FixedDensity/CountExtraction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.cyclicAPMass line 11
  2. def OAI.Erdos3.FixedDensity.cyclicAPDiagonalMass line 15
  3. def OAI.Erdos3.FixedDensity.cyclicAPOffDiagMass line 19
  4. theorem OAI.Erdos3.FixedDensity.cyclicAPProduct_zero_difference line 26
  5. theorem OAI.Erdos3.FixedDensity.cyclicAPDiagonalMass_eq_sum_pow line 31
  6. theorem OAI.Erdos3.FixedDensity.pow_le_pow_pred_mul line 36
  7. theorem OAI.Erdos3.FixedDensity.cyclicAPDiagonalMass_le line 47
  8. theorem OAI.Erdos3.FixedDensity.cyclicAPMass_eq_diagonal_add_offDiagMass line 67
  9. theorem OAI.Erdos3.FixedDensity.cyclicAPOffDiagMass_pos_of_diagonal_lt_mass line 89
  10. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_eq_mass_div_div line 98
  11. theorem OAI.Erdos3.FixedDensity.cyclicAPMass_eq_mul_mul_count line 105
  12. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_eq_diagonal_add_offDiagMass_div_div line 114
  13. theorem OAI.Erdos3.FixedDensity.cyclicAPOffDiagMass_nonneg line 122
  14. theorem OAI.Erdos3.FixedDensity.cyclicAPOffDiagMass_pos_of_count line 133
  15. theorem OAI.Erdos3.FixedDensity.cyclicAPProduct_pos_iff_of_nonneg line 157
  16. theorem OAI.Erdos3.FixedDensity.exists_cyclicAP_of_offDiagMass_pos line 174