OAI/NumberTheory/Jacobsthal/Sieve/IntegerResidueVariance.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.AdditiveLargeSieve.exponential line 17
  2. theorem OAI.Erdos970.AdditiveLargeSieve.monomial_eq_exponential line 19
  3. theorem OAI.Erdos970.AdditiveLargeSieve.monomial_add line 26
  4. theorem OAI.Erdos970.AdditiveLargeSieve.monomial_norm line 29
  5. theorem OAI.Erdos970.AdditiveLargeSieve.shifted_sum_norm line 32
  6. theorem OAI.Erdos970.AdditiveLargeSieve.separated_consecutive_bound line 45
  7. theorem OAI.Erdos970.AdditiveLargeSieve.additive_large_sieve line 75
  8. def OAI.Erdos970.ErdosInverseSpectrum.residueCount line 109
  9. def OAI.Erdos970.ErdosInverseSpectrum.spectrum line 112
  10. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_eq_sum line 115
  11. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_zero line 119
  12. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_orthogonality line 122
  13. theorem OAI.Erdos970.ErdosInverseSpectrum.conjugate_spectrum line 129
  14. theorem OAI.Erdos970.ErdosInverseSpectrum.residue_weighted_sum line 148
  15. theorem OAI.Erdos970.ErdosInverseSpectrum.residue_count_sum line 161
  16. theorem OAI.Erdos970.ErdosInverseSpectrum.residue_square_sum line 166
  17. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_conjugate_sum line 180
  18. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_parseval line 195
  19. theorem OAI.Erdos970.ErdosInverseSpectrum.centered_residue_variance line 201
  20. def OAI.Erdos970.ErdosInverseSpectrum.exponentialSum line 236
  21. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_eq_exponentialSum line 239
  22. theorem OAI.Erdos970.ErdosInverseSpectrum.spectrum_eq_exponentialSum_val line 252
  23. theorem OAI.Erdos970.ErdosInverseSpectrum.residue_values_univ line 265
  24. theorem OAI.Erdos970.ErdosInverseSpectrum.sum_over_residues line 275
  25. theorem OAI.Erdos970.ErdosInverseSpectrum.residue_values_nonzero line 281
  26. theorem OAI.Erdos970.ErdosInverseSpectrum.sum_over_nonzero_residues line 304
  27. theorem OAI.Erdos970.ErdosInverseSpectrum.centered_variance_exponential line 310
  28. def OAI.Erdos970.ErdosInverseSpectrum.integerResidueCount line 327
  29. def OAI.Erdos970.ErdosInverseSpectrum.integerResidueVariance line 330
  30. theorem OAI.Erdos970.ErdosInverseSpectrum.residueCount_at_val line 333
  31. theorem OAI.Erdos970.ErdosInverseSpectrum.variance_eq_integerResidueVariance line 348
  32. theorem OAI.Erdos970.ErdosInverseSpectrum.integer_variance_fourier line 353