OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrefixAverage.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.prefixAverage line 31
  2. def OAI.OrdinaryCorrelations.absPrimeDefect line 34
  3. def OAI.OrdinaryCorrelations.absDefect line 37
  4. def OAI.OrdinaryCorrelations.magnitude line 40
  5. lemma OAI.OrdinaryCorrelations.norm_magnitude line 42
  6. lemma OAI.OrdinaryCorrelations.magnitude_oneBounded line 46
  7. lemma OAI.OrdinaryCorrelations.magnitude_multiplicative line 51
  8. lemma OAI.OrdinaryCorrelations.absPrimeDefect_nonneg line 56
  9. lemma OAI.OrdinaryCorrelations.absDefect_eq_sum line 63
  10. lemma OAI.OrdinaryCorrelations.absDefect_tendsto line 76
  11. lemma OAI.OrdinaryCorrelations.absDefect_le_distanceSq line 85
  12. theorem OAI.OrdinaryCorrelations.magnitude_uniformlyNonpretentious line 104
  13. theorem OAI.OrdinaryCorrelations.prefixAverage_tendsto_zero line 119
  14. theorem OAI.OrdinaryCorrelations.magnitude_mean_zero line 134
  15. lemma OAI.OrdinaryCorrelations.prefixAverage_translation_bound line 140
  16. lemma OAI.OrdinaryCorrelations.translation_mean_error_tendsto line 147
  17. theorem OAI.OrdinaryCorrelations.prefixAverage_translation_tendsto line 157
  18. lemma OAI.OrdinaryCorrelations.sum_magnitude_norm line 163
  19. lemma OAI.OrdinaryCorrelations.prefixAverage_magnitude_norm line 171
  20. theorem OAI.OrdinaryCorrelations.absolute_defect_mean_zero line 175
  21. lemma OAI.OrdinaryCorrelations.shiftAverage_comm line 181
  22. lemma OAI.OrdinaryCorrelations.shiftAverage_norm_le_magnitude_mean line 186
  23. theorem OAI.OrdinaryCorrelations.shiftAverage_of_divergent_defect line 199
  24. theorem OAI.OrdinaryCorrelations.divergent_absolute_defect_correlation line 209
  25. lemma OAI.OrdinaryCorrelations.positive_zero_of_zero_at_one line 218
  26. theorem OAI.OrdinaryCorrelations.shiftAverage_of_zero_at_one line 224
  27. theorem OAI.OrdinaryCorrelations.zero_at_one_correlation line 239
  28. theorem OAI.OrdinaryCorrelations.shiftAverage_translation_error_tendsto line 247
  29. theorem OAI.OrdinaryCorrelations.positive_gap_of_failure line 259
  30. theorem OAI.OrdinaryCorrelations.normalized_finite_defects_of_failure line 276
  31. theorem OAI.OrdinaryCorrelations.biased_sequence_of_failure line 296