OAI/NumberTheory/DirichletL/CubicSieve/LogarithmicTargets.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.secondLogTargets line 84
  2. lemma OAI.SecondPassArithmetic.secondLogTargets_mem line 92
  3. lemma OAI.SecondPassArithmetic.secondLogTargets_bounds line 101
  4. lemma OAI.SecondPassArithmetic.secondLogSector_coordinates line 115
  5. lemma OAI.SecondPassArithmetic.secondSupportedSector_remainder_bound line 134
  6. lemma OAI.SecondPassArithmetic.secondSupportedSector_eq_empty line 144
  7. theorem OAI.SecondPassArithmetic.truncatedSecondSource_eq_binned line 166
  8. theorem OAI.SecondPassArithmetic.truncatedSecondSource_norm_le_binned line 207
  9. lemma OAI.SecondPassArithmetic.supported_cutoff_denominator line 242
  10. def OAI.SecondPassArithmetic.firstCoreSecondRowBound line 255
  11. theorem OAI.SecondPassArithmetic.firstCoreSecondCutoff_supported_row_bound line 261
  12. theorem OAI.SecondPassArithmetic.normalized_binned_second_density_transfer line 317
  13. theorem OAI.SecondPassArithmetic.firstCoreInputRow_binned_finite_transfer line 409
  14. lemma OAI.CubicEisenstein.quadraticHeightDenominator_continuous line 516
  15. lemma OAI.CubicEisenstein.rowSmoothPower_continuousAt line 521
  16. lemma OAI.CubicEisenstein.rowLogD_continuousAt line 531
  17. lemma OAI.CubicEisenstein.rowLogDD_continuousAt line 550
  18. def OAI.CubicEisenstein.smoothFirstCoefficient line 571
  19. def OAI.CubicEisenstein.smoothSecondCoefficient line 573
  20. lemma OAI.CubicEisenstein.smoothFirstCoefficient_eq_deriv line 576
  21. lemma OAI.CubicEisenstein.smoothSecondCoefficient_eq_deriv line 587
  22. lemma OAI.CubicEisenstein.smoothCoefficients_continuousAt line 598
  23. lemma OAI.CubicEisenstein.spatial_summable_derivative_bounds line 616
  24. def OAI.CubicEisenstein.eisensteinFirstPartial line 659
  25. def OAI.CubicEisenstein.eisensteinSecondPartial line 662
  26. lemma OAI.CubicEisenstein.eisensteinPartials_eq_tsum line 665
  27. lemma OAI.CubicEisenstein.actual_spatial_continuousAt line 680