OAI/NumberTheory/DirichletL/Moments/SecondLedger.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondLedger.nonzero_unequal_min_six line 14
  2. def OAI.SevenEighths.CenteredMomentSecondLedger.localSaving line 36
  3. theorem OAI.SevenEighths.CenteredMomentSecondLedger.localSaving_lower line 42
  4. theorem OAI.SevenEighths.CenteredMomentSecondLedger.actual_localSaving_lower line 75
  5. theorem OAI.SevenEighths.CenteredMomentSecondLedger.local_nonzero_of_global line 87
  6. theorem OAI.SevenEighths.CenteredMomentSecondLedger.log_norm_power_product line 119
  7. def OAI.SevenEighths.CenteredMomentSecondLedger.secondSaving line 128
  8. def OAI.SevenEighths.CenteredMomentSecondLedger.actualUnitSet line 132
  9. def OAI.SevenEighths.CenteredMomentSecondLedger.actualNonunitSet line 135
  10. theorem OAI.SevenEighths.CenteredMomentSecondLedger.log_norm_radical line 139
  11. theorem OAI.SevenEighths.CenteredMomentSecondLedger.secondSaving_eq_norm_ledger line 147
  12. theorem OAI.SevenEighths.CenteredMomentSecondLedger.actual_secondSaving_lower line 192