OAI/NumberTheory/DirichletL/CubicSieve/SecondPoisson.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.masked_pair_second_poisson line 83
  2. def OAI.SecondPassArithmetic.secondGaussTerm line 168
  3. def OAI.SecondPassArithmetic.actualSecondKernel line 177
  4. def OAI.SecondPassArithmetic.secondLogTest line 188
  5. theorem OAI.SecondPassArithmetic.secondGaussTerm_log_twist line 193
  6. theorem OAI.SecondPassArithmetic.actualSecondKernel_eq_integral line 207
  7. theorem OAI.SecondPassArithmetic.secondChildSum_continuous line 292
  8. theorem OAI.SecondPassArithmetic.secondChildSum_uniform_bound line 303
  9. theorem OAI.SecondPassArithmetic.secondTotalEnergy_nonneg line 318
  10. theorem OAI.SecondPassArithmetic.secondTotalEnergy_continuous line 325
  11. theorem OAI.SecondPassArithmetic.secondTotalEnergy_uniform_bound line 338
  12. theorem OAI.SecondPassArithmetic.secondTotalEnergy_integrable line 357
  13. theorem OAI.SecondPassArithmetic.second_integral_norm_le_energy line 369
  14. theorem OAI.SecondPassArithmetic.secondLogTest_continuous line 443
  15. theorem OAI.SecondPassArithmetic.secondLogTest_norm line 449
  16. def OAI.SecondPassArithmetic.secondKernelEnergy line 454
  17. theorem OAI.SecondPassArithmetic.actual_second_kernel_uniform_energy_envelope line 459
  18. theorem OAI.SecondPassArithmetic.second_energy_selected_family line 509
  19. def OAI.SecondPassArithmetic.tupleLabelElement line 550
  20. theorem OAI.SecondPassArithmetic.tupleLabelElement_span line 553
  21. theorem OAI.SecondPassArithmetic.exists_label_unit line 557
  22. def OAI.SecondPassArithmetic.tupleLabelUnit line 563
  23. theorem OAI.SecondPassArithmetic.tupleLabelUnit_spec line 566
  24. def OAI.SecondPassArithmetic.fixedChildRow line 575
  25. def OAI.SecondPassArithmetic.idealChildRow line 579
  26. theorem OAI.SecondPassArithmetic.tuple_child_eq_unit_sector line 584
  27. theorem OAI.SecondPassArithmetic.fixed_child_second_energy_pushforward line 592
  28. theorem OAI.SecondPassArithmetic.idealChildRow_unit_energy_le line 617