OAI/NumberTheory/PrimePackets/CuspMass.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.cusp_indicator_le_siegel line 44
  2. lemma OAI.PrimeDegreePackets.cusp_mass_le_cube_moment line 67
  3. lemma OAI.PrimeDegreePackets.right_ball_indicator_le_siegel line 78
  4. lemma OAI.PrimeDegreePackets.right_ball_mass_le_box_moment line 102
  5. lemma OAI.PrimeDegreePackets.open_mass_le_of_probability_limit line 116
  6. theorem OAI.PrimeDegreePackets.packet_ball_bound_bounded_discr line 133
  7. def OAI.PrimeDegreePackets.packetProbability line 173
  8. theorem OAI.PrimeDegreePackets.packet_limit_ball_bound_bounded_discr line 181
  9. def OAI.PrimeDegreePackets.logMomentConstant line 208
  10. lemma OAI.PrimeDegreePackets.logMoment_summable line 211
  11. lemma OAI.PrimeDegreePackets.logMomentConstant_nonneg line 227
  12. lemma OAI.PrimeDegreePackets.logarithmic_shell line 230
  13. theorem OAI.PrimeDegreePackets.log_weighted_sum_le line 245
  14. theorem OAI.PrimeDegreePackets.log_weighted_sum_cutoff line 303
  15. lemma OAI.PrimeDegreePackets.cusp_log_error_vanishes line 357
  16. lemma OAI.PrimeDegreePackets.cube_fiber_log_rectangle line 370
  17. lemma OAI.PrimeDegreePackets.cube_fiber_product_le line 400
  18. theorem OAI.PrimeDegreePackets.productFiberIntegral_cube_eq_zero line 416
  19. theorem OAI.PrimeDegreePackets.productFiberIntegral_cube_le line 432