OAI/NumberTheory/DirichletL/Moments/ActiveDivisorShell.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.CenteredMomentActiveDivisorShell.Source line 14
  2. def OAI.SevenEighths.CenteredMomentActiveDivisorShell.Source.active line 38
  3. def OAI.SevenEighths.CenteredMomentActiveDivisorShell.Source.allowance line 42
  4. theorem OAI.SevenEighths.CenteredMomentActiveDivisorShell.Source.active_boundary line 45
  5. theorem OAI.SevenEighths.CenteredMomentActiveDivisorShell.reciprocal_sqrt_log line 51
  6. theorem OAI.SevenEighths.CenteredMomentActiveDivisorShell.Source.active_pair_weight line 60
  7. theorem OAI.SevenEighths.CenteredMomentActiveDivisorShell.paired_active_divisor_shell line 82
  8. theorem OAI.SevenEighths.CenteredMomentActiveDivisorShell.paired_all_active_shell line 106