OAI/Combinatorics/Progressions/Estimates/FiniteProductCellMean.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.finiteCellMean line 11
  2. theorem OAI.Erdos3.finiteCellMean_sum line 15
  3. def OAI.Erdos3.finiteCellWeights line 24
  4. def OAI.Erdos3.finiteCellResidueMean line 30
  5. theorem OAI.Erdos3.finite_cell_energy_aggregate line 35
  6. theorem OAI.Erdos3.uniform_subtype_mean line 54
  7. theorem OAI.Erdos3.uniform_observedProductDensity_conditional line 66
  8. theorem OAI.Erdos3.finiteCellMean_uniform line 96
  9. theorem OAI.Erdos3.finiteCellWeights_uniform line 103
  10. theorem OAI.Erdos3.finiteCellMean_uniform_weighted line 116
  11. theorem OAI.Erdos3.finiteCellResidueMean_uniform line 124
  12. theorem OAI.Erdos3.uniform_cell_residue_bound line 138
  13. theorem OAI.Erdos3.uniform_cell_energy_aggregate line 148
  14. theorem OAI.Erdos3.finiteCellMean_product line 173
  15. theorem OAI.Erdos3.finiteCellWeights_product line 187
  16. theorem OAI.Erdos3.finiteCellMean_product_uniform line 201