OAI/NumberTheory/DirichletL/Eisenstein/SeedDefects.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cuspSeed_row_defect line 78
  2. theorem OAI.CubicEisenstein.heightPoincare_cuspSeed_laplace_defect line 87
  3. def OAI.CubicEisenstein.smoothCuspSeedField line 119
  4. def OAI.CubicEisenstein.smoothCuspSeedDefectField line 123
  5. lemma OAI.CubicEisenstein.smoothCuspSeedField_eq line 127
  6. lemma OAI.CubicEisenstein.smoothCuspSeedDefectField_eq line 131
  7. lemma OAI.CubicEisenstein.actual_smoothCuspSeed_contDiffAt line 136
  8. theorem OAI.CubicEisenstein.actual_smoothCuspSeed_laplace_defect line 143
  9. lemma OAI.CubicEisenstein.cuspSeedProfile_entire line 151
  10. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_entire line 154
  11. lemma OAI.CubicEisenstein.cuspCutoffCorrection_parameter_entire line 158
  12. theorem OAI.CubicEisenstein.smoothCuspSeed_entire line 177
  13. theorem OAI.CubicEisenstein.smoothCuspSeedDefect_entire line 181
  14. def OAI.CanonicalQuadraticSieve.sectorBadIdeal line 194
  15. theorem OAI.CanonicalQuadraticSieve.sector_bad_good_product line 196
  16. theorem OAI.CanonicalQuadraticSieve.sectorBadIdeal_ne_zero_of_row line 202
  17. def OAI.CanonicalQuadraticSieve.unrestrictedPairTerm line 212
  18. theorem OAI.CanonicalQuadraticSieve.unrestrictedPairTerm_sector line 218
  19. def OAI.CanonicalQuadraticSieve.unrestrictedDualTruncatedMiddle line 239
  20. theorem OAI.CanonicalQuadraticSieve.unrestrictedDualTruncatedMiddle_sector line 249
  21. lemma OAI.CanonicalQuadraticSieve.divisorEnergyFactor_mono_coefficients line 301
  22. lemma OAI.CanonicalQuadraticSieve.dual_bad_sector_scale line 314
  23. def OAI.CanonicalQuadraticSieve.dualMiddleMajorant line 337
  24. lemma OAI.CanonicalQuadraticSieve.dualMiddleMajorant_nonneg line 345
  25. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_truncated_middle_sector line 360
  26. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.unrestricted_dual_truncated_middle line 456
  27. theorem OAI.SecondPassArithmetic.secondChildColumn_fixed_mask line 509
  28. theorem OAI.SecondPassArithmetic.fixedChildRow_fixed_pool line 516
  29. theorem OAI.SecondPassIntegration.childEnergy_fixed_pool line 539
  30. theorem OAI.SecondPassIntegration.childGeometricMean_fixed_pool line 545
  31. theorem OAI.SecondPassIntegration.densityChildEnergy_fixed_pool line 551
  32. theorem OAI.SecondPassIntegration.restored_child_mask_norm line 562
  33. lemma OAI.SecondPassArithmetic.element_norm_le_of_dvd line 579
  34. lemma OAI.SecondPassArithmetic.primeProduct_ne_zero line 591
  35. lemma OAI.SecondPassArithmetic.squarefreeLabel_active_bound line 596
  36. lemma OAI.SecondPassArithmetic.jLabel_dvd_cube_product line 617
  37. lemma OAI.SecondPassArithmetic.b0_square_dvd_cube_product line 629
  38. lemma OAI.SecondPassArithmetic.b0_jLabel_square line 636
  39. theorem OAI.SecondPassArithmetic.cube_label_norm_bounds line 647