OAI/NumberTheory/DirichletL/PrincipalSignalComparison.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.PrincipalSignalComparison.raw_inverse_ae_reciprocal line 16
  2. theorem OAI.SevenEighths.PrincipalSignalComparison.raw_quotient_integral_eq line 26
  3. def OAI.SevenEighths.PrincipalSignalComparison.slotMass line 35
  4. def OAI.SevenEighths.PrincipalSignalComparison.slotProduct line 37
  5. def OAI.SevenEighths.PrincipalSignalComparison.slotRatio line 41
  6. structure OAI.SevenEighths.PrincipalSignalComparison.SlotBounds line 45
  7. def OAI.SevenEighths.PrincipalSignalComparison.slotErrorConstant line 55
  8. theorem OAI.SevenEighths.PrincipalSignalComparison.slot_scalar_ne_zero line 57
  9. theorem OAI.SevenEighths.PrincipalSignalComparison.slotRatio_error line 62
  10. theorem OAI.SevenEighths.PrincipalSignalComparison.slotRatio_bound line 72
  11. theorem OAI.SevenEighths.PrincipalSignalComparison.principalSlot_differentiableAt line 80
  12. theorem OAI.SevenEighths.PrincipalSignalComparison.slotRatio_continuous_line line 110
  13. def OAI.SevenEighths.PrincipalSignalComparison.slotResidue line 129
  14. theorem OAI.SevenEighths.PrincipalSignalComparison.slotResidue_eq_reciprocal line 136
  15. def OAI.SevenEighths.PrincipalSignalComparison.kernel line 150
  16. def OAI.SevenEighths.PrincipalSignalComparison.kernelEnvelope line 153
  17. theorem OAI.SevenEighths.PrincipalSignalComparison.kernel_continuous line 156
  18. theorem OAI.SevenEighths.PrincipalSignalComparison.kernel_norm_bound line 165
  19. theorem OAI.SevenEighths.PrincipalSignalComparison.kernel_integrable line 181
  20. theorem OAI.SevenEighths.PrincipalSignalComparison.slotResidue_bound_of_reciprocal_bound line 192
  21. theorem OAI.SevenEighths.PrincipalSignalComparison.exists_slotResidue_bound line 256
  22. theorem OAI.SevenEighths.PrincipalSignalComparison.raw_slot_integrable line 275
  23. instance OAI.SevenEighths.PrincipalSignalComparison.(instance at line 289) line 289
  24. theorem OAI.SevenEighths.PrincipalSignalComparison.idealCoeff_norm_one_of_coprime line 291
  25. theorem OAI.SevenEighths.PrincipalSignalComparison.prime_coprime_of_norm_gt line 305
  26. def OAI.SevenEighths.PrincipalSignalComparison.annularPrimeWeight line 316
  27. theorem OAI.SevenEighths.PrincipalSignalComparison.annularPrimeWeight_nonneg line 319
  28. theorem OAI.SevenEighths.PrincipalSignalComparison.annularPrimeWeight_norm_lower line 323
  29. theorem OAI.SevenEighths.PrincipalSignalComparison.annularPrimeWeight_target_unit line 328
  30. def OAI.SevenEighths.PrincipalSignalComparison.sourceCorrection line 336
  31. theorem OAI.SevenEighths.PrincipalSignalComparison.sourceCorrection_eq_principal line 339
  32. theorem OAI.SevenEighths.PrincipalSignalComparison.sourceCorrection_differentiable line 344
  33. theorem OAI.SevenEighths.PrincipalSignalComparison.sourceCorrection_bound line 349
  34. def OAI.SevenEighths.PrincipalSignalComparison.actualSlotResidue line 354
  35. theorem OAI.SevenEighths.PrincipalSignalComparison.actual_principal_slot line 361
  36. theorem OAI.SevenEighths.PrincipalSignalComparison.exists_actualSlotResidue_bound line 370
  37. theorem OAI.SevenEighths.PrincipalSignalComparison.source_normalizer_cast line 396
  38. theorem OAI.SevenEighths.PrincipalSignalComparison.source_normalizer_ne_zero line 405
  39. theorem OAI.SevenEighths.PrincipalSignalComparison.source_power_identity line 411
  40. theorem OAI.SevenEighths.PrincipalSignalComparison.normalized_source_double_residue line 421
  41. def OAI.SevenEighths.PrincipalSignalComparison.sourceResidueIntegral line 447
  42. theorem OAI.SevenEighths.PrincipalSignalComparison.sourceResidueIntegral_normalized line 452
  43. theorem OAI.SevenEighths.PrincipalSignalComparison.source_double_residue_integrable line 473
  44. def OAI.SevenEighths.PrincipalSignalComparison.activePools line 494
  45. theorem OAI.SevenEighths.PrincipalSignalComparison.slotMass_active line 497
  46. theorem OAI.SevenEighths.PrincipalSignalComparison.slotProduct_active line 505
  47. theorem OAI.SevenEighths.PrincipalSignalComparison.slotRatio_active line 515
  48. theorem OAI.SevenEighths.PrincipalSignalComparison.slotResidue_active line 520
  49. theorem OAI.SevenEighths.PrincipalSignalComparison.slotResidue_isBigO line 525
  50. theorem OAI.SevenEighths.PrincipalSignalComparison.actualSlotResidue_isBigO line 558
  51. theorem OAI.SevenEighths.PrincipalSignalComparison.fixedPrincipal_product_eq line 576
  52. theorem OAI.SevenEighths.PrincipalSignalComparison.exists_normalized_actual_source_bound line 580