OAI/NumberTheory/DirichletL/CubicSieve/DensityBudgets.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.canonicalDensityConstant line 88
  2. theorem OAI.SecondPassArithmetic.canonicalDensityConstant_nonneg line 91
  3. theorem OAI.SecondPassArithmetic.globalFirstQuantitativeBudget_state_bound line 98
  4. def OAI.SecondPassArithmetic.canonicalRankMass line 171
  5. theorem OAI.SecondPassArithmetic.canonicalRankMass_initial line 174
  6. theorem OAI.SecondPassArithmetic.canonicalRankMass_step line 178
  7. theorem OAI.SecondPassArithmetic.canonicalRankMass_child line 186
  8. theorem OAI.SecondPassArithmetic.canonicalRankMass_global line 192
  9. theorem OAI.SecondPassArithmetic.lowerCubeBin_transfer_mass line 201
  10. theorem OAI.SecondPassArithmetic.lowerCubeBin_energy_normalization line 209
  11. theorem OAI.SecondPassArithmetic.canonical_live_scale_bounds line 222
  12. theorem OAI.SecondPassArithmetic.canonical_small_or_live line 228
  13. def OAI.SecondPassArithmetic.canonicalPoolCutoff line 237
  14. theorem OAI.SecondPassArithmetic.canonicalPoolCutoff_covers line 239
  15. def OAI.CanonicalRowCompletion.rowFamilyEnergy line 261
  16. theorem OAI.CanonicalRowCompletion.rowFamilyEnergy_eq_sum line 264
  17. theorem OAI.CanonicalRowCompletion.rowFamilyEnergy_nonneg line 273
  18. theorem OAI.CanonicalRowCompletion.rowFamilyEnergy_integral_polynomial line 279
  19. theorem OAI.CanonicalRowCompletion.rowFamilyEnergy_const_mul line 325
  20. theorem OAI.CanonicalRowCompletion.canonicalSmoothedEnergy_eq_rowFamilyEnergy line 335
  21. theorem OAI.CanonicalRowCompletion.separated_canonical_integrable line 361
  22. theorem OAI.CanonicalRowCompletion.separated_canonical_family_energy line 378
  23. theorem OAI.CanonicalRowCompletion.rowFamilyEnergy_bound_sum line 419
  24. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_family_binned_energy line 453
  25. theorem OAI.CanonicalRowCompletion.outsideCanonicalBin_energy line 482
  26. theorem OAI.SecondPassArithmetic.canonicalProgress_large line 542
  27. theorem OAI.SecondPassArithmetic.paddedCanonicalRatio line 549
  28. def OAI.SecondPassArithmetic.canonicalRankMargin line 553
  29. theorem OAI.SecondPassArithmetic.canonicalRankMargin_lower line 556
  30. theorem OAI.SecondPassArithmetic.canonicalRankMargin_step line 562
  31. theorem OAI.SecondPassArithmetic.canonicalRatio_exp_loss line 570
  32. theorem OAI.SecondPassArithmetic.canonicalRankMargin_padding line 574
  33. theorem OAI.SecondPassArithmetic.fixedTripleMask_ne_zero_of_bin line 595
  34. theorem OAI.SecondPassArithmetic.canonical_retained_scale_closure line 610
  35. theorem OAI.SecondPassArithmetic.canonical_retained_unpadded_closure line 666