OAI/NumberTheory/Ostmann/Characters/TemplateOneSidedNumericInputsGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.coefficient_pow_exp_le line 9
  2. theorem OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.sum_three_le_exp line 23
  3. def OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.rowLogHeight line 32
  4. def OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.rowHeightCoefficient line 35
  5. def OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.numericCostCoefficient line 37
  6. theorem OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.rowHeightCoefficient_pos line 40
  7. theorem OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.row_height_le_exp line 45
  8. theorem OAI.Ostmann.Characters.TemplateOneSidedNumericInputs.numeric_inputs_cost line 73