OAI/Analysis/CharacterCriterion/JiangSu.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KirchbergRordam.JiangSu.StepParameters line 41
  2. def OAI.KirchbergRordam.JiangSu.parameters line 55
  3. instance OAI.KirchbergRordam.JiangSu.(instance at line 72) line 72
  4. instance OAI.KirchbergRordam.JiangSu.(instance at line 74) line 74
  5. lemma OAI.KirchbergRordam.JiangSu.initial_sizes line 79
  6. lemma OAI.KirchbergRordam.JiangSu.next_sizes line 81
  7. lemma OAI.KirchbergRordam.JiangSu.lower_count line 86
  8. lemma OAI.KirchbergRordam.JiangSu.upper_count line 92
  9. lemma OAI.KirchbergRordam.JiangSu.middle_count line 97
  10. lemma OAI.KirchbergRordam.JiangSu.number_eigenpaths line 105
  11. def OAI.KirchbergRordam.JiangSu.Stage line 114
  12. instance OAI.KirchbergRordam.JiangSu.(instance at line 115) line 115
  13. instance OAI.KirchbergRordam.JiangSu.(instance at line 117) line 117
  14. def OAI.KirchbergRordam.JiangSu.connecting line 119
  15. lemma OAI.KirchbergRordam.JiangSu.connecting_norm line 121
  16. lemma OAI.KirchbergRordam.JiangSu.connecting_formula line 125
  17. def OAI.KirchbergRordam.JiangSu.inclusion line 133
  18. lemma OAI.KirchbergRordam.JiangSu.inclusion_norm line 134
  19. lemma OAI.KirchbergRordam.JiangSu.inclusion_connecting line 136
  20. lemma OAI.KirchbergRordam.JiangSu.dense_stages line 139
  21. lemma OAI.KirchbergRordam.JiangSu.algebra_is_recipe_limit line 143
  22. theorem OAI.KirchbergRordam.JiangSu.equiv_arithmetic_presentation line 146
  23. def OAI.KirchbergRordam.PrimeDropPresentation.stageTrace line 154
  24. theorem OAI.KirchbergRordam.PrimeDropPresentation.trace_exists line 157
  25. theorem OAI.KirchbergRordam.PrimeDropPresentation.trace_unique line 159
  26. theorem OAI.KirchbergRordam.PrimeDropPresentation.projectionless line 163
  27. theorem OAI.KirchbergRordam.JiangSu.hom_injective line 176
  28. theorem OAI.KirchbergRordam.JiangSu.trace_exists line 179
  29. theorem OAI.KirchbergRordam.JiangSu.trace_unique line 181
  30. theorem OAI.KirchbergRordam.JiangSu.projectionless line 183
  31. theorem OAI.KirchbergRordam.JiangSu.no_characters line 186