OAI/NumberTheory/DirichletL/Poisson/PrincipalTruncation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TruncatedPrincipalPoisson.mem_rowNormDisk_floor line 79
  2. theorem OAI.TruncatedPrincipalPoisson.dualNear_eq_finite line 95
  3. theorem OAI.TruncatedPrincipalPoisson.dualFar_decay line 109
  4. theorem OAI.TruncatedPrincipalPoisson.middle_divisor_frequency_tail line 155
  5. def OAI.TruncatedPrincipalPoisson.principalTruncation line 226
  6. def OAI.TruncatedPrincipalPoisson.middleTruncation line 233
  7. def OAI.TruncatedPrincipalPoisson.truncationError line 239
  8. theorem OAI.TruncatedPrincipalPoisson.truncationError_eq line 244
  9. theorem OAI.TruncatedPrincipalPoisson.truncationError_bound line 258
  10. lemma OAI.JointLogSeparation.schwartz_phase_inversion line 320
  11. lemma OAI.JointLogSeparation.product_three_integrals line 325
  12. def OAI.JointLogSeparation.profileSourceBound line 331
  13. lemma OAI.JointLogSeparation.profileSourceBound_nonneg line 336
  14. lemma OAI.JointLogSeparation.source_le_profileSourceBound line 341
  15. lemma OAI.JointLogSeparation.profile_fourier_envelope line 353
  16. theorem OAI.JointLogSeparation.joint_separation_identity line 363
  17. theorem OAI.JointLogSeparation.joint_separation_envelope line 392
  18. lemma OAI.JointLogSeparation.seven_phase_factor line 446
  19. def OAI.JointLogSeparation.outerWindow line 457
  20. def OAI.JointLogSeparation.fixedColumnTest line 460
  21. theorem OAI.JointLogSeparation.seven_kernel_separation line 462
  22. lemma OAI.JointLogSeparation.weighted_schwartz_integrable line 519
  23. lemma OAI.JointLogSeparation.density_weight_identity line 523
  24. lemma OAI.JointLogSeparation.triple_product_integral_bound line 529
  25. theorem OAI.JointLogSeparation.triple_coefficient_moment_bound line 547
  26. abbrev OAI.FiniteOverlapDecomposition.Triple line 590
  27. def OAI.FiniteOverlapDecomposition.triples line 592
  28. def OAI.FiniteOverlapDecomposition.split line 595
  29. def OAI.FiniteOverlapDecomposition.join line 598
  30. lemma OAI.FiniteOverlapDecomposition.join_split line 601
  31. lemma OAI.FiniteOverlapDecomposition.split_mem line 610
  32. lemma OAI.FiniteOverlapDecomposition.join_mem line 627
  33. lemma OAI.FiniteOverlapDecomposition.split_join line 636
  34. theorem OAI.FiniteOverlapDecomposition.sum_pair_eq_overlap line 664