OAI/NumberTheory/DirichletL/MeanSquare/SourceRemainders.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InitialMeanSquare.initialHighRadialCost line 86
  2. theorem OAI.InitialMeanSquare.initial_high_radial_sum line 109
  3. theorem OAI.InitialMeanSquare.initial_log_harmonic_polynomial line 153
  4. theorem OAI.InitialMeanSquare.initial_high_radial_order line 172
  5. theorem OAI.InitialMeanSquare.initial_high_radial_negligible line 179
  6. theorem OAI.InitialMeanSquare.initialErrorFrequencyBound_le line 244
  7. def OAI.InitialMeanSquare.initialErrorRowBound line 288
  8. lemma OAI.InitialMeanSquare.initialErrorRowBound_pos line 291
  9. theorem OAI.InitialMeanSquare.initialErrorRowBound_valid line 297
  10. def OAI.InitialMeanSquare.initialPolynomialCap line 312
  11. lemma OAI.InitialMeanSquare.initialPolynomialCap_ge_one line 316
  12. theorem OAI.InitialMeanSquare.initial_actual_bin_polynomial_caps line 322
  13. theorem OAI.InitialMeanSquare.initial_two_windows_bounded line 358
  14. theorem OAI.InitialMeanSquare.initial_high_radial_source line 381
  15. lemma OAI.FirstPassCubeLabels.threeBlockExponent_ne_zero_on line 480
  16. lemma OAI.FirstPassCubeLabels.threeBlockExponent_lt_six_on line 491
  17. lemma OAI.FirstPassCubeLabels.threeGaussRowFactor_norm_le line 497
  18. lemma OAI.FirstPassCubeLabels.canonicalPairMode_norm_le line 520
  19. theorem OAI.FirstPassCubeLabels.full_uniform_canonicalPairMode_remainder line 550
  20. def OAI.FirstPassCubeLabels.canonicalFirstFrequencyRadius line 608
  21. theorem OAI.FirstPassCubeLabels.firstFrequencyDisk_uniform line 613
  22. theorem OAI.FirstPassCubeLabels.full_uniform_canonicalPairMode_disk_remainder line 663