OAI/NumberTheory/DirichletL/CubicSieve/ConjugateProfiles.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecondPassIntegration.logPhase_conjugate line 77
  2. theorem OAI.SecondPassIntegration.conjugateProfile_frequencyTwist line 85
  3. theorem OAI.SecondPassIntegration.normalized_conjugate_frequencyTwist line 91
  4. theorem OAI.SecondPassIntegration.normalized_conjugate_profile_envelope line 97
  5. theorem OAI.JointLogSeparation.seven_kernel_twisted_profiles line 115
  6. theorem OAI.SecondPassArithmetic.secondPreColumn_zero_of_common_overlap line 188
  7. theorem OAI.SecondPassArithmetic.weighted_secondChildKernelPair_congr_off_common line 197
  8. theorem OAI.SecondPassArithmetic.weighted_secondRayChild_congr_off_common line 254
  9. theorem OAI.SecondPassArithmetic.secondChildKernelPair_eq_of_quotient_span line 284
  10. theorem OAI.SecondPassArithmetic.secondChildKernelPair_const_kernel line 295
  11. theorem OAI.SecondPassArithmetic.weighted_secondRayChild_normalized line 322
  12. def OAI.SecondPassArithmetic.secondExpansionQuotient line 377
  13. theorem OAI.SecondPassArithmetic.secondExpansionQuotient_of_subset line 382
  14. def OAI.SecondPassArithmetic.secondExpansionScale line 387
  15. def OAI.SecondPassArithmetic.secondExpansionPushWeight line 393
  16. theorem OAI.SecondPassArithmetic.secondExpansionPushWeight_sum line 398
  17. theorem OAI.SecondPassArithmetic.secondExpansionPushWeight_at_source line 421
  18. def OAI.SecondPassArithmetic.secondExpansionSource line 435
  19. def OAI.SecondPassArithmetic.secondNormalizedExpansionWeight line 449
  20. theorem OAI.SecondPassArithmetic.secondExpansionSource_eq_raw_variable_sector line 458
  21. theorem OAI.SecondPassArithmetic.secondInputCoefficient_norm_le line 504
  22. theorem OAI.SecondPassArithmetic.secondNormalizedExpansionWeight_after_scale line 515
  23. theorem OAI.SecondPassArithmetic.secondNormalizedExpansionWeight_norm_le line 536
  24. theorem OAI.SecondPassArithmetic.secondNormalizedPushWeight_norm_le line 566
  25. lemma OAI.CubicEisenstein.isUnit_quotient_span_iff line 589
  26. abbrev OAI.CubicEisenstein.AffineUnitResidue line 609
  27. lemma OAI.CubicEisenstein.affine_representative_condition line 612
  28. def OAI.CubicEisenstein.affineResidueMap line 618
  29. lemma OAI.CubicEisenstein.affineResidueMap_bijective line 628
  30. def OAI.CubicEisenstein.affineResidueEquiv line 665
  31. def OAI.CubicEisenstein.unitsSubtypeEquiv line 668
  32. def OAI.CubicEisenstein.quotientProductEquiv line 674
  33. def OAI.CubicEisenstein.affineCRTEq line 679
  34. lemma OAI.CubicEisenstein.affine_ramified_unit line 686
  35. def OAI.CubicEisenstein.affineRamifiedEquiv line 695
  36. def OAI.CubicEisenstein.affineUnramifiedEquiv line 698
  37. def OAI.CubicEisenstein.idealTotient line 708
  38. lemma OAI.CubicEisenstein.card_admissible_ramified_product line 710
  39. lemma OAI.CubicEisenstein.absNorm_span_lambda line 723
  40. lemma OAI.CubicEisenstein.card_quotient_lambda_pow line 730
  41. theorem OAI.CubicEisenstein.card_admissible_lambda_pow_mul line 735