OAI/NumberTheory/DirichletL/MeanSquare/LogarithmicBins.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InitialMeanSquare.initialOuterWeight line 84
  2. lemma OAI.InitialMeanSquare.initialOuterWeight_continuous line 89
  3. lemma OAI.InitialMeanSquare.initialOuterWeight_norm line 101
  4. def OAI.InitialMeanSquare.initialSourceSum line 112
  5. theorem OAI.InitialMeanSquare.initialSource_eq_integrated line 118
  6. theorem OAI.InitialMeanSquare.initial_source_uniform_transfer line 180
  7. def OAI.InitialMeanSquare.initialLogIndex line 234
  8. def OAI.InitialMeanSquare.initialLogColumn line 238
  9. def OAI.InitialMeanSquare.initialLogLabel line 241
  10. lemma OAI.InitialMeanSquare.sourceRow_nonzero line 244
  11. lemma OAI.InitialMeanSquare.sourceLabel_span line 248
  12. lemma OAI.InitialMeanSquare.sourceLabel_norm line 255
  13. lemma OAI.InitialMeanSquare.sourceQuotient_nonzero line 262
  14. theorem OAI.InitialMeanSquare.initial_log_coordinates line 272
  15. theorem OAI.InitialMeanSquare.initial_log_target_bounds line 323
  16. theorem OAI.InitialMeanSquare.initial_log_mass line 336
  17. theorem OAI.InitialMeanSquare.initial_log_radial line 343
  18. theorem OAI.InitialMeanSquare.sourceLabel_squarefree line 363
  19. theorem OAI.InitialMeanSquare.sourceMask_coprime line 371
  20. theorem OAI.InitialMeanSquare.initialLogIndex_mem_box line 387
  21. theorem OAI.InitialMeanSquare.initial_log_box_small_power line 399
  22. theorem OAI.SecondPassArithmetic.local_first_conductor_balance line 431
  23. theorem OAI.SecondPassArithmetic.local_first_conductor_bound line 436
  24. theorem OAI.SecondPassArithmetic.firstActiveProduct_as_primeProduct line 447
  25. theorem OAI.SecondPassArithmetic.first_conductor_product_balance line 457
  26. theorem OAI.SecondPassArithmetic.first_conductor_product_dvd line 471
  27. theorem OAI.SecondPassArithmetic.first_conductor_norm_bound line 486
  28. lemma OAI.SecondPassArithmetic.first_row_numeric_bound line 512
  29. theorem OAI.SecondPassArithmetic.globalFirstRowScale_le_pooled line 534
  30. theorem OAI.SecondPassArithmetic.first_row_enlargement line 562
  31. def OAI.SecondPassArithmetic.globalFirstFrequencyScale line 611
  32. def OAI.SecondPassArithmetic.globalCubeFirstTargets line 618
  33. theorem OAI.SecondPassArithmetic.globalCubeFirstTargets_mem line 624
  34. theorem OAI.SecondPassArithmetic.globalCubeFirstTargets_ne_zero line 633
  35. theorem OAI.SecondPassArithmetic.globalCubeFirstTargets_norm_bound line 643