OAI/NumberTheory/DirichletL/Mellin/CompactScale.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompactScaleBridge.realCompactOutsideSum line 50
  2. theorem OAI.CompactScaleBridge.realCompactOutsideSum_bound_of_fixedTestPrimeMS line 56
  3. theorem OAI.CompactScaleBridge.realCompactOutsideSum_isBigO_of_fixedTestPrimeMS line 127
  4. structure OAI.CompactScaleBridge.FixedTestPrimeMSConstants line 148
  5. def OAI.CompactScaleBridge.FixedTestPrimeMSConstants.absorb line 174
  6. theorem OAI.CompactScaleBridge.realCompactOutsideSum_isBigO_of_fixedTestPrimeMSConstants line 227
  7. theorem OAI.CompactMellinBridge.compact_weight_mellin_convergent line 262
  8. theorem OAI.CompactMellinBridge.weighted_term_integrable line 281
  9. theorem OAI.CompactMellinBridge.weighted_sum_continuousOn_pos line 298
  10. theorem OAI.CompactMellinBridge.weighted_sum_inv_locallyIntegrableOn_pos line 344
  11. theorem OAI.CompactMellinBridge.weighted_norm_scale line 360
  12. theorem OAI.CompactMellinBridge.weighted_norm_integral line 376
  13. theorem OAI.CompactMellinBridge.weighted_terms_fubini line 425
  14. def OAI.CompactMellinBridge.finiteEulerFactor line 438
  15. theorem OAI.CompactMellinBridge.finiteEulerFactor_analytic line 445
  16. theorem OAI.CompactMellinBridge.zero_free_of_analytic_identity_gt_two line 466
  17. theorem OAI.CompactMellinBridge.zero_free_of_regularized_identity_gt_two line 491
  18. theorem OAI.CompactMellinBridge.outsideCoeff_baseChange_zero line 513
  19. def OAI.CompactMellinBridge.outsideCompactSum line 534
  20. theorem OAI.CompactMellinBridge.outsideCompactSum_hasSum line 540
  21. theorem OAI.CompactMellinBridge.outside_compact_euler_identity line 564
  22. theorem OAI.CompactMellinBridge.pair_zero_free_of_identity_gt_two line 613
  23. theorem OAI.CompactMellinBridge.baseChange_outsideCompact_zero_free line 716
  24. structure OAI.CompactMellinBridge.BaseChangeOutsideCompactTest line 779
  25. theorem OAI.CompactMellinBridge.dirichletTarget_of_compact_outside_tests line 793