OAI/NumberTheory/DirichletL/CubicSieve/FixedProfiles.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.secondGaussTerm_test_factors line 84
  2. theorem OAI.SecondPassArithmetic.secondFrequencyKernel_log_tests line 92
  3. theorem OAI.SecondPassIntegration.radialPairKernel_dyadic_normalization line 122
  4. theorem OAI.SecondPassIntegration.secondChildKernelPair_eq_postCommon line 150
  5. theorem OAI.SecondPassIntegration.halfNormalization_support_bound line 204
  6. lemma OAI.SecondPassIntegration.translated_support_bound line 214
  7. theorem OAI.SecondPassIntegration.exists_fixed_sector_windows line 224
  8. theorem OAI.SecondPassIntegration.exists_fixed_normalized_child_tests line 251
  9. def OAI.SecondPassArithmetic.actualSecondRawSector line 312
  10. theorem OAI.SecondPassArithmetic.actualSecondRawSector_fixed_profiles line 327
  11. theorem OAI.SecondPassArithmetic.activeGaussRowFactor_zero_of_ne line 379
  12. theorem OAI.SecondPassArithmetic.activeGaussRowFactor_empty line 391
  13. theorem OAI.SecondPassArithmetic.secondGaussTerm_empty line 398
  14. theorem OAI.SecondPassArithmetic.secondFrequencyKernel_zero line 409
  15. lemma OAI.CubicEisenstein.symbol_cube_numerator line 447
  16. theorem OAI.CubicEisenstein.arithmeticResidueSum_cube line 454
  17. lemma OAI.CubicEisenstein.admissibleResidue_nonempty line 467
  18. theorem OAI.CubicEisenstein.arithmeticResidueSum_cube_ne_zero line 471
  19. lemma OAI.CubicEisenstein.denominatorCondition_congr line 478
  20. lemma OAI.CubicEisenstein.denominatorCondition_mul line 485
  21. lemma OAI.CubicEisenstein.row_symbol_congr_modulus line 490
  22. lemma OAI.CubicEisenstein.denominatorRep_product_congr line 497
  23. def OAI.CubicEisenstein.residueMultiplication line 503
  24. lemma OAI.CubicEisenstein.denominatorCondition_coprime_modulus line 509
  25. lemma OAI.CubicEisenstein.residueMultiplication_injective line 515
  26. def OAI.CubicEisenstein.residueMultiplicationEquiv line 527
  27. lemma OAI.CubicEisenstein.residueMultiplication_phase line 534
  28. lemma OAI.CubicEisenstein.arithmeticResidueSum_zero line 544
  29. theorem OAI.CubicEisenstein.arithmeticResidueSum_constant_eigen line 550
  30. theorem OAI.CubicEisenstein.arithmeticResidueSum_ne_zero_forces_trivial line 565
  31. lemma OAI.CubicEisenstein.coprime_of_dvd_sub_one line 582
  32. lemma OAI.CubicEisenstein.primary_coprime_three line 586
  33. lemma OAI.CubicEisenstein.exists_one_mod_and_prescribed line 589
  34. theorem OAI.CubicEisenstein.constant_coefficient_primary_prime_exponent line 595