OAI/Analysis/MarkovType/AlternatingNorm.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.C00.alternating line 16
  2. def OAI.MarkovSuperreflexivity.C00.alternatingArray line 19
  3. def OAI.MarkovSuperreflexivity.C00.alternatingEven line 21
  4. def OAI.MarkovSuperreflexivity.C00.alternatingOdd line 24
  5. theorem OAI.MarkovSuperreflexivity.C00.alternating_zero line 27
  6. theorem OAI.MarkovSuperreflexivity.C00.alternating_one line 30
  7. theorem OAI.MarkovSuperreflexivity.C00.alternatingArray_even line 33
  8. theorem OAI.MarkovSuperreflexivity.C00.alternatingArray_odd line 37
  9. theorem OAI.MarkovSuperreflexivity.C00.place_alternatingArray line 41
  10. theorem OAI.MarkovSuperreflexivity.C00.alternating_eq_ofArray line 62
  11. theorem OAI.MarkovSuperreflexivity.C00.alternating_apply line 69
  12. theorem OAI.MarkovSuperreflexivity.C00.alternating_apply_zero line 83
  13. theorem OAI.MarkovSuperreflexivity.C00.alternating_ne_zero line 89
  14. def OAI.MarkovSuperreflexivity.C00.shift line 94
  15. theorem OAI.MarkovSuperreflexivity.C00.shift_zero line 97
  16. theorem OAI.MarkovSuperreflexivity.C00.shift_basis line 100
  17. theorem OAI.MarkovSuperreflexivity.C00.shift_apply_add line 103
  18. theorem OAI.MarkovSuperreflexivity.C00.shift_apply_add_right line 108
  19. theorem OAI.MarkovSuperreflexivity.C00.shift_apply_lt line 112
  20. theorem OAI.MarkovSuperreflexivity.C00.shift_ofArray line 120
  21. theorem OAI.MarkovSuperreflexivity.C00.shift_alternating line 126
  22. theorem OAI.MarkovSuperreflexivity.C00.alternating_add line 135
  23. def OAI.MarkovSuperreflexivity.C00.alternatingPlacement line 147
  24. theorem OAI.MarkovSuperreflexivity.C00.alternatingPlacement_even line 154
  25. theorem OAI.MarkovSuperreflexivity.C00.alternatingPlacement_odd line 171
  26. theorem OAI.MarkovSuperreflexivity.C00.alternatingPlacement_strictMono line 188
  27. def OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm line 216
  28. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_zero line 218
  29. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_nonneg line 222
  30. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_pos line 225
  31. theorem OAI.MarkovSuperreflexivity.OrderedNorm.placed_alternatingNorm line 231
  32. theorem OAI.MarkovSuperreflexivity.OrderedNorm.placed_alternating_pairs_norm line 237
  33. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingPairs_norm line 245
  34. theorem OAI.MarkovSuperreflexivity.OrderedNorm.shift_alternatingNorm line 254
  35. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_subadditive line 261
  36. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_twice_le line 273
  37. theorem OAI.MarkovSuperreflexivity.OrderedNorm.basis_sub_basis_norm line 277