OAI/NumberTheory/PiExponent/Analysis/LiteralAnalyticSummand.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.LiteralAnalytic.fixedWeights line 12
  2. abbrev OAI.PiExponent.LiteralAnalytic.Transverse line 15
  3. def OAI.PiExponent.LiteralAnalytic.beta line 18
  4. abbrev OAI.PiExponent.LiteralAnalytic.RowChoice line 21
  5. abbrev OAI.PiExponent.LiteralAnalytic.ChoiceFamily line 25
  6. def OAI.PiExponent.LiteralAnalytic.indexWeight line 28
  7. def OAI.PiExponent.LiteralAnalytic.rowWeight line 31
  8. def OAI.PiExponent.LiteralAnalytic.choiceScalar line 34
  9. def OAI.PiExponent.LiteralAnalytic.choiceMatrix line 43
  10. theorem OAI.PiExponent.LiteralAnalytic.fixedWeights_pos line 49
  11. theorem OAI.PiExponent.LiteralAnalytic.fixedWeights_lower line 55
  12. theorem OAI.PiExponent.LiteralAnalytic.rowOrder_le line 61
  13. theorem OAI.PiExponent.LiteralAnalytic.indexWeight_nonneg line 70
  14. theorem OAI.PiExponent.LiteralAnalytic.indexWeight_le line 75
  15. theorem OAI.PiExponent.LiteralAnalytic.norm_choiceScalar_le line 79
  16. theorem OAI.PiExponent.LiteralAnalytic.rowWeight_le_indexWeight_of_ne_zero line 109
  17. theorem OAI.PiExponent.LiteralAnalytic.actualRowCount_pos line 117
  18. theorem OAI.PiExponent.LiteralAnalytic.sum_rowWeight_eq line 122
  19. theorem OAI.PiExponent.LiteralAnalytic.low_transverse_capacity line 133
  20. theorem OAI.PiExponent.LiteralAnalytic.lowIndexCount_pos line 155
  21. theorem OAI.PiExponent.LiteralAnalytic.norm_scalar_product_le line 163
  22. theorem OAI.PiExponent.LiteralAnalytic.norm_choiceMatrix_le line 177
  23. theorem OAI.PiExponent.LiteralAnalytic.norm_actual_summand_le line 201