OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MeanC.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.SourceRoughFourier.meanC line 31
  2. def OAI.OrdinaryCorrelations.SourceRoughFourier.meanR line 33
  3. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanC_add line 35
  4. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanC_sum line 39
  5. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanC_mul_left line 44
  6. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.mean_char line 49
  7. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.poly_mul line 61
  8. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.mean_poly line 74
  9. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.mean_poly_mul line 84
  10. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.conjugate_poly line 92
  11. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanR_cast line 99
  12. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.parseval line 104
  13. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanR_nonneg line 124
  14. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanR_mono line 129
  15. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanR_sum line 134
  16. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.energy_real line 139
  17. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.fourth_moment_real line 151
  18. def OAI.OrdinaryCorrelations.SourceRoughFourier.additiveEnergy line 167
  19. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.fourth_moment_le_energy line 172
  20. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.low_high_frequency_bound line 202
  21. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.natCast_inj_of_lt line 274
  22. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.mean_poly_three line 283
  23. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.short_convolution line 293
  24. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.interval_parseval_bound line 329
  25. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.norm_meanC_le line 344
  26. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.norm_poly_le line 349
  27. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.norm_poly_le_card line 356
  28. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.sum_eq_mul_meanR line 364
  29. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.meanR_cauchy line 368
  30. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.low_high_mean_bound line 382
  31. def OAI.OrdinaryCorrelations.SourceRoughFourier.natEnergyQuadruples line 411
  32. def OAI.OrdinaryCorrelations.SourceRoughFourier.natAdditiveEnergy line 414
  33. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.energy_natCast_eq line 418
  34. def OAI.OrdinaryCorrelations.SourceRoughFourier.predicateTriples line 437
  35. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.energy_le_predicate_triples line 443
  36. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.reciprocal_poly_norm_le line 474
  37. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.reciprocal_poly_norm_le_count line 480
  38. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.reciprocal_fourth_moment_le line 492
  39. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.sum_Icc_one_eq_range line 506
  40. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.prefix_translation_bound line 517
  41. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.averaged_prefix_translation_bound line 540
  42. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.shortEnvelope_bound line 566
  43. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.shortEnvelope_nonneg line 574
  44. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.interval_parseval_neg_bound line 578
  45. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.rough_correlation_bound line 593
  46. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.abs_liouville_le_one line 681
  47. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.progressionCoeff_norm_le line 692
  48. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.liouville_rough_shift_bound line 699
  49. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.natAdditiveEnergy_mono line 732
  50. def OAI.OrdinaryCorrelations.SourceRoughFourier.IsRough line 738
  51. def OAI.OrdinaryCorrelations.SourceRoughFourier.roughIntegers line 741
  52. def OAI.OrdinaryCorrelations.SourceRoughFourier.roughTriples line 745
  53. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.energy_le_roughTriples line 750
  54. theorem OAI.OrdinaryCorrelations.SourceRoughFourier.reciprocal_mass_le_rough_count line 762