OAI/Combinatorics/SumProduct/Alignment/Admissible01.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceAdmissible.previous line 44
  2. structure OAI.SourceAdmissible.Parameters line 49
  3. def OAI.SourceAdmissible.Parameters.L line 74
  4. lemma OAI.SourceAdmissible.Parameters.Xpos line 76
  5. lemma OAI.SourceAdmissible.Parameters.Wdiv line 81
  6. lemma OAI.SourceAdmissible.Parameters.Wle line 84
  7. lemma OAI.SourceAdmissible.Parameters.Lpos line 87
  8. lemma OAI.SourceAdmissible.Parameters.Lbound line 90
  9. lemma OAI.SourceAdmissible.Parameters.Lsmooth line 94
  10. lemma OAI.SourceAdmissible.Parameters.Xtendsto line 100
  11. lemma OAI.SourceAdmissible.Parameters.XoverL line 104
  12. lemma OAI.SourceAdmissible.Parameters.eventual_X line 109
  13. lemma OAI.SourceAdmissible.Parameters.eventual_J line 114
  14. lemma OAI.SourceAdmissible.Parameters.exists_tail line 120
  15. structure OAI.SourceAdmissible.TailBound line 134
  16. lemma OAI.SourceAdmissible.Parameters.exists_tailBound line 138
  17. def OAI.SourceAdmissible.normalized line 145
  18. lemma OAI.SourceAdmissible.added_is_block line 167
  19. def OAI.SourceAdmissible.pivotScales line 175
  20. def OAI.SourceAdmissible.shiftModel line 217
  21. def OAI.SourceAdmissible.Parameters.models line 226
  22. lemma OAI.SourceAdmissible.shift_models line 230
  23. def OAI.SourceAdmissible.Parameters.law line 237
  24. theorem OAI.SourceAdmissible.admissible_charted_alignment line 243