OAI/NumberTheory/DirichletL/CubicSieve/UniformTransfer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.full_uniform_labeled_child_second_energy_pushforward line 81
  2. theorem OAI.SecondPassArithmetic.full_uniform_fixed_second_mode_transfer line 117
  3. theorem OAI.SecondPassIntegration.full_uniform_integrated_fixed_second_mode_transfer line 177
  4. theorem OAI.SecondPassArithmetic.full_uniform_postCommonSmoothPair_fixed_tests line 243
  5. theorem OAI.SecondPassIntegration.full_uniform_tupleSource_transfer line 273
  6. theorem OAI.SecondPassArithmetic.full_uniform_globalSecondSource_transfer line 331
  7. theorem OAI.SecondPassArithmetic.full_uniform_globalSecondRawSource_transfer line 395
  8. theorem OAI.SecondPassArithmetic.full_uniform_globalArithmeticBin_transfer line 427
  9. theorem OAI.SecondPassArithmetic.full_uniform_postCommonSmoothPair_twisted_fixed_tests line 490
  10. theorem OAI.SecondPassIntegration.full_uniform_tupleSource_twisted_transfer line 523
  11. theorem OAI.SecondPassArithmetic.full_uniform_globalSecondSource_twisted_transfer line 584
  12. theorem OAI.SecondPassArithmetic.full_uniform_globalSecondRawSource_twisted_transfer line 650
  13. theorem OAI.SecondPassArithmetic.full_uniform_globalArithmeticBin_twisted_transfer line 682