OAI/NumberTheory/DirichletL/Moments/SecondPhysicalLedger.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.physicalBlock_effective_window line 21
  2. lemma OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.logb_one_add_sixth line 38
  3. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.scalar_log_ledger line 44
  4. def OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.forcingNorm line 72
  5. def OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.saving line 76
  6. def OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.centralPhysicalCost line 84
  7. lemma OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.common_product_pos line 92
  8. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.actual_physical_log_ledger line 101
  9. lemma OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.centralPhysicalCost_pos line 151
  10. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.actual_physical_cost_bound line 168
  11. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.actual_canonical_physical_cost line 184
  12. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.physicalBlock_canonical_witness line 201
  13. theorem OAI.SevenEighths.CenteredMomentSecondPhysicalLedger.original_block_physical_cost line 233