OAI/NumberTheory/DirichletL/Moments/WholeDivisorShell.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.divisorPool_nonzero_norm line 15
  2. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.moebius_norm_le_one line 25
  3. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.squarefree_of_moebius_ne_zero line 30
  4. def OAI.SevenEighths.CenteredMomentWholeDivisorShell.live line 34
  5. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.mem_live line 36
  6. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.live_squarefree line 39
  7. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.live_norm_one line 42
  8. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.sum_moebius_live line 45
  9. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.sum_norm_moebius_live line 55
  10. def OAI.SevenEighths.CenteredMomentWholeDivisorShell.normKey line 65
  11. def OAI.SevenEighths.CenteredMomentWholeDivisorShell.shell line 66
  12. def OAI.SevenEighths.CenteredMomentWholeDivisorShell.selectedShells line 67
  13. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.normKey_eq_iff line 69
  14. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.mem_shell_iff line 78
  15. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.shell_disjoint line 90
  16. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.shell_nonempty_iff line 96
  17. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.biUnion_shell line 105
  18. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.sum_moebius_shells line 114
  19. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.sum_norm_moebius_shells line 120
  20. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.selected_scale_bounds line 126
  21. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.selected_subset_indices line 141
  22. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.selected_card_log line 149
  23. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.selected_card_subpower line 160
  24. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.divisorPool_card_log line 184
  25. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.divisorPool_card_subpower line 190
  26. lemma OAI.SevenEighths.CenteredMomentWholeDivisorShell.shell_member_data line 201
  27. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.finite_pair_mobius_shells line 209
  28. theorem OAI.SevenEighths.CenteredMomentWholeDivisorShell.divisorPool_weighted_shells line 217