OAI/NumberTheory/PrimePackets/ThetaTails.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_uniform_exponential_bound line 91
  2. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_joint_stronglyMeasurable line 150
  3. def OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail line 169
  4. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_eq_zero line 172
  5. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_stronglyMeasurable line 176
  6. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_bounds line 181
  7. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_locallyIntegrable line 210
  8. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_bigO_zero line 223
  9. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_mellin_differentiable line 233
  10. def OAI.PrimeDegreePackets.ThetaConstruction.logScaleLinearEquiv line 254
  11. def OAI.PrimeDegreePackets.ThetaConstruction.logScale line 268
  12. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_apply line 271
  13. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_symm_apply line 274
  14. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_symm line 277
  15. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_norm_le line 281
  16. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScale_opNorm_le line 291
  17. def OAI.PrimeDegreePackets.ThetaConstruction.logScaledLattice line 296
  18. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScaledLattice_inverse_bound line 299
  19. lemma OAI.PrimeDegreePackets.ThetaConstruction.logScaledLattice_measurable_apply line 315
  20. theorem OAI.PrimeDegreePackets.ThetaConstruction.logScaledLattice_averaged_mellin_differentiable line 325
  21. def OAI.PrimeDegreePackets.restoredLogCoordinates line 350
  22. lemma OAI.PrimeDegreePackets.restoredLogCoordinates_exp line 353
  23. lemma OAI.PrimeDegreePackets.restoredLogCoordinates_continuous line 357
  24. lemma OAI.PrimeDegreePackets.restoredLogCoordinates_bound_on_compact line 365
  25. def OAI.PrimeDegreePackets.arithmeticFlowThetaTail line 381
  26. lemma OAI.PrimeDegreePackets.arithmeticFlowTheta_vector line 387
  27. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaTail_boundedAverage_entire line 400
  28. def OAI.PrimeDegreePackets.orderedThetaLogDomain line 426
  29. theorem OAI.PrimeDegreePackets.orderedThetaLogDomain_fundamental line 431
  30. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaTail_unitAverage_entire line 436
  31. theorem OAI.PrimeDegreePackets.orderedThetaLogDomain_volume line 444
  32. def OAI.PrimeDegreePackets.ThetaConstruction.exponentialTail line 455
  33. lemma OAI.PrimeDegreePackets.ThetaConstruction.exponentialTail_mellinConvergent line 458
  34. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_uniform_majorant line 475
  35. theorem OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_mellin_integrableProd line 489
  36. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_mellin_integrable line 517
  37. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_mellin_eq_integral line 528