OAI/NumberTheory/DirichletL/CubicSieve/NormalizedMass.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.columnLog_norm_lower line 88
  2. theorem OAI.SecondPassArithmetic.normalized_second_coefficient_sq_le line 95
  3. theorem OAI.SecondPassArithmetic.normalized_second_mass_zero line 110
  4. theorem OAI.SecondPassArithmetic.normalized_second_mass_fixed_bound line 126
  5. theorem OAI.SecondPassArithmetic.full_uniform_normalized_second_mass line 175
  6. def OAI.SecondPassArithmetic.globalFirstColumnMass line 199
  7. theorem OAI.SecondPassArithmetic.globalFirstColumnMass_support line 207
  8. theorem OAI.SecondPassArithmetic.globalFirstColumnMass_zero_off_support line 247
  9. theorem OAI.SecondPassArithmetic.globalFirstDiagonalCost_eq_supported line 257
  10. theorem OAI.SecondPassArithmetic.globalDiagonalPowers line 279
  11. theorem OAI.SecondPassArithmetic.globalFirstDiagonalCost_parent_bound line 312
  12. theorem OAI.CompletedGauss.bracket_one_eq_quadratic line 416
  13. theorem OAI.CompletedGauss.quadratic_value_cube line 433
  14. theorem OAI.CompletedGauss.residual_bracket_cube line 449
  15. theorem OAI.CompletedGauss.residual_bracket_product line 459
  16. theorem OAI.CompletedGauss.powerful_inverse_norm_sum line 471
  17. theorem OAI.CompletedGauss.prime_square_dvd_powerful line 532
  18. theorem OAI.CompletedGauss.nonresidual_prime_square_dvd line 544
  19. def OAI.CompletedGauss.nonresidualGain line 554
  20. theorem OAI.CompletedGauss.nonresidual_gain_product_dvd line 556
  21. def OAI.CompletedGauss.completedLocalExponent line 588
  22. def OAI.CompletedGauss.reflectionExtractedPrime line 591
  23. def OAI.CompletedGauss.reflectionExtractedDivisor line 594
  24. def OAI.CompletedGauss.reflectionConductorCost line 598
  25. def OAI.CompletedGauss.reflectionLocalCost line 605
  26. theorem OAI.CompletedGauss.reflectionConductorCost_eq_prod line 609
  27. theorem OAI.CompletedGauss.reflectionLocalCost_nonneg line 627
  28. theorem OAI.CompletedGauss.reflectionLocalCost_le_square line 632
  29. theorem OAI.CompletedGauss.reflectionLocalCost_le_single line 643
  30. theorem OAI.CompletedGauss.completedLocalExponent_of_not_dvd line 653
  31. theorem OAI.CompletedGauss.reflectionLocalCost_le_gain line 661
  32. theorem OAI.CompletedGauss.reflectionConductorCost_bound line 672