OAI/NumberTheory/Ostmann/Characters/DiagonalEstimateCodeFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.DiagonalEstimate.codePreservingMatchings line 14
  2. theorem OAI.Ostmann.Characters.DiagonalEstimate.mem_codePreservingMatchings line 18
  3. theorem OAI.Ostmann.Characters.DiagonalEstimate.codePreservingMatchings_card_le line 24
  4. def OAI.Ostmann.Characters.DiagonalEstimate.sourceNonbulkCount line 32
  5. theorem OAI.Ostmann.Characters.DiagonalEstimate.sourceNonbulkCount_pos line 34
  6. def OAI.Ostmann.Characters.DiagonalEstimate.sourceNonbulkLogCost line 38
  7. theorem OAI.Ostmann.Characters.DiagonalEstimate.sourceNonbulkLogCost_exp line 41
  8. theorem OAI.Ostmann.Characters.DiagonalEstimate.copiedNonbulk_card_le_sourceNonbulkCount line 45
  9. theorem OAI.Ostmann.Characters.DiagonalEstimate.codePreservingMatchings_card_le_exp line 54
  10. theorem OAI.Ostmann.Characters.DiagonalEstimate.codePreserving_normalized_factor_le line 67