OAI/NumberTheory/PrimePackets/HaarUniqueness.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.rightAction_transitive line 57
  2. theorem OAI.PrimeDegreePackets.isHaarProbability_unique line 66
  3. lemma OAI.PrimeDegreePackets.idealCoefficient_abscissa_le_one line 84
  4. lemma OAI.PrimeDegreePackets.dedekindZeta_differentiableAt line 90
  5. def OAI.PrimeDegreePackets.regularizedDedekindZeta line 102
  6. def OAI.PrimeDegreePackets.logRegularizedDedekindZeta line 105
  7. lemma OAI.PrimeDegreePackets.regularizedDedekindZeta_pos line 108
  8. lemma OAI.PrimeDegreePackets.regularizedDedekindZeta_differentiableAt line 115
  9. lemma OAI.PrimeDegreePackets.logRegularizedDedekindZeta_differentiableAt line 124
  10. lemma OAI.PrimeDegreePackets.tendsto_regularizedDedekindZeta line 128
  11. lemma OAI.PrimeDegreePackets.tendsto_logRegularizedDedekindZeta line 134
  12. theorem OAI.PrimeDegreePackets.residue_log_comparison_of_deriv_bound line 141
  13. theorem OAI.PrimeDegreePackets.residue_comparison_of_deriv_bound line 165
  14. def OAI.PrimeDegreePackets.realPoleKernel line 196
  15. lemma OAI.PrimeDegreePackets.realPoleKernel_nonneg line 198
  16. theorem OAI.PrimeDegreePackets.realPoleKernel_comparison line 204
  17. theorem OAI.PrimeDegreePackets.tsum_realPoleKernel_comparison line 246
  18. theorem OAI.PrimeDegreePackets.fieldDiscriminant_le_packetScale_sq line 267
  19. theorem OAI.PrimeDegreePackets.weightedIdeal_realInterval_of_zeta_scale line 281
  20. def OAI.PrimeDegreePackets.UniformZetaScaleBound line 319
  21. theorem OAI.PrimeDegreePackets.packet_box_moment_of_zeta_scale line 332
  22. theorem OAI.PrimeDegreePackets.packet_cube_moment_of_zeta_scale line 372
  23. theorem OAI.PrimeDegreePackets.packet_ball_bound_of_zeta_scale line 409
  24. theorem OAI.PrimeDegreePackets.packet_limit_ball_bound_of_zeta_scale line 449
  25. theorem OAI.PrimeDegreePackets.packet_tight_of_zeta_scale line 470
  26. theorem OAI.PrimeDegreePackets.packet_probability_subsequence_of_zeta_scale line 524
  27. theorem OAI.PrimeDegreePackets.packet_limit_positive_ergodic_components_of_zeta_scale line 555