OAI/NumberTheory/DirichletL/MeanSquare/HighRadialBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InitialMeanSquare.initial_squarefree_target_geometry line 84
  2. theorem OAI.InitialMeanSquare.initialSquarefreeBinCost_of_density_bound line 115
  3. lemma OAI.InitialMeanSquare.initial_bin_row_scale_le line 178
  4. theorem OAI.InitialMeanSquare.initial_bin_cost_uniform line 188
  5. theorem OAI.InitialMeanSquare.outside_prime_divisor_mem_pool line 238
  6. theorem OAI.InitialMeanSquare.outside_factors_mem_pool line 253
  7. theorem OAI.InitialMeanSquare.outside_prime_mem_pool line 263
  8. def OAI.InitialMeanSquare.initialElementaryConstant line 283
  9. lemma OAI.InitialMeanSquare.initialElementaryConstant_nonneg line 285
  10. theorem OAI.InitialMeanSquare.initial_child_energy_elementary line 298
  11. theorem OAI.InitialMeanSquare.initial_child_geometric_elementary line 324
  12. theorem OAI.InitialMeanSquare.initial_subbin_target_bounds line 356
  13. theorem OAI.InitialMeanSquare.initial_subbin_geometric_elementary line 379
  14. def OAI.InitialMeanSquare.initialRestrictedBinCost line 414
  15. lemma OAI.InitialMeanSquare.initialRestrictedBinCost_full line 428
  16. theorem OAI.InitialMeanSquare.initial_subbin_density_elementary line 448
  17. theorem OAI.InitialMeanSquare.initial_subbin_cost_elementary line 495
  18. def OAI.InitialMeanSquare.initialRadial line 533
  19. theorem OAI.InitialMeanSquare.initial_radial_absorbs_rows line 536
  20. def OAI.InitialMeanSquare.initialHighRadialConstant line 559
  21. lemma OAI.InitialMeanSquare.initialHighRadialConstant_nonneg line 562
  22. theorem OAI.InitialMeanSquare.initial_subbin_cost_radial_decay line 578