OAI/NumberTheory/OrdinaryCorrelations/Elliott/SmoothCutoffExists.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrdinaryCorrelations.RawCutoff.smooth_cutoff_exists line 45
  2. lemma OAI.OrdinaryCorrelations.RawCutoff.avg_instances line 60
  3. lemma OAI.OrdinaryCorrelations.RawCutoff.avg_product_finset line 66
  4. lemma OAI.OrdinaryCorrelations.RawCutoff.avg_coordinate line 83
  5. lemma OAI.OrdinaryCorrelations.RawCutoff.avg_two_coordinates line 89
  6. lemma OAI.OrdinaryCorrelations.RawCutoff.avg_centered_sum_sq line 95
  7. def OAI.OrdinaryCorrelations.RawCutoff.count line 109
  8. def OAI.OrdinaryCorrelations.RawCutoff.mean line 112
  9. lemma OAI.OrdinaryCorrelations.RawCutoff.count_variance line 114
  10. lemma OAI.OrdinaryCorrelations.RawCutoff.count_deviation line 138
  11. lemma OAI.OrdinaryCorrelations.RawCutoff.cutoff_deficit line 147
  12. lemma OAI.OrdinaryCorrelations.RawCutoff.cutoff_mean_deficit line 158
  13. def OAI.OrdinaryCorrelations.RawCutoff.primeSystem line 175
  14. lemma OAI.OrdinaryCorrelations.RawCutoff.primeSystem_mean line 181
  15. lemma OAI.OrdinaryCorrelations.RawCutoff.count_integer line 185
  16. lemma OAI.OrdinaryCorrelations.RawCutoff.ordinary_deficit_mean line 194
  17. lemma OAI.OrdinaryCorrelations.RawCutoff.product_cutoff_error line 211
  18. lemma OAI.OrdinaryCorrelations.RawCutoff.cutoff_mean_omission line 246
  19. lemma OAI.OrdinaryCorrelations.RawCutoff.Pā‚€_eq_source line 267
  20. lemma OAI.OrdinaryCorrelations.RawCutoff.defect_scale_tendsto line 271
  21. theorem OAI.OrdinaryCorrelations.RawCutoff.source_cutoff_error line 289