OAI/Analysis/CharacterCriterion/BalancedSystem.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KirchbergRordam.BalancedDropMultiplicity.upper line 33
  2. def OAI.KirchbergRordam.BalancedDropMultiplicity.lower line 34
  3. def OAI.KirchbergRordam.BalancedDropMultiplicity.middle line 35
  4. def OAI.KirchbergRordam.BalancedDropMultiplicity.next line 37
  5. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.lower_eq line 39
  6. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.upper_pos line 42
  7. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.lower_pos line 43
  8. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.lower_two line 46
  9. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.sum_le_product line 49
  10. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.total line 53
  11. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.next_two line 56
  12. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.mul_upper line 57
  13. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.mul_lower line 58
  14. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.at_zero line 61
  15. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.at_one line 69
  16. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.zero_space line 79
  17. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.one_space line 82
  18. def OAI.KirchbergRordam.BalancedDropMultiplicity.stage line 86
  19. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.stage_zero line 89
  20. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.stage_succ line 90
  21. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.stage_two line 92
  22. lemma OAI.KirchbergRordam.BalancedDropMultiplicity.stage_coprime line 96
  23. lemma OAI.KirchbergRordam.MatrixBlockReindex.reindex_trans line 107
  24. lemma OAI.KirchbergRordam.MatrixBlockReindex.reindex_block line 118
  25. lemma OAI.KirchbergRordam.MatrixBlockReindex.reindex_left line 126
  26. lemma OAI.KirchbergRordam.MatrixBlockReindex.reindex_right line 134
  27. abbrev OAI.KirchbergRordam.BalancedDropSystem.P line 151
  28. abbrev OAI.KirchbergRordam.BalancedDropSystem.Q line 152
  29. abbrev OAI.KirchbergRordam.BalancedDropSystem.Low line 153
  30. abbrev OAI.KirchbergRordam.BalancedDropSystem.High line 154
  31. abbrev OAI.KirchbergRordam.BalancedDropSystem.Mid line 155
  32. abbrev OAI.KirchbergRordam.BalancedDropSystem.Slot line 156
  33. abbrev OAI.KirchbergRordam.BalancedDropSystem.Index line 157
  34. abbrev OAI.KirchbergRordam.BalancedDropSystem.ZeroSpace line 158
  35. abbrev OAI.KirchbergRordam.BalancedDropSystem.OneSpace line 159
  36. def OAI.KirchbergRordam.BalancedDropSystem.zeroLow line 162
  37. def OAI.KirchbergRordam.BalancedDropSystem.zeroMid line 164
  38. def OAI.KirchbergRordam.BalancedDropSystem.zeroOuter line 166
  39. def OAI.KirchbergRordam.BalancedDropSystem.oneLow line 168
  40. def OAI.KirchbergRordam.BalancedDropSystem.oneMid line 170
  41. def OAI.KirchbergRordam.BalancedDropSystem.oneOuter line 172
  42. def OAI.KirchbergRordam.BalancedDropSystem.slotSwap line 176
  43. def OAI.KirchbergRordam.BalancedDropSystem.zeroReindex line 182
  44. def OAI.KirchbergRordam.BalancedDropSystem.oneReindex line 185
  45. lemma OAI.KirchbergRordam.BalancedDropSystem.half_mem line 190
  46. def OAI.KirchbergRordam.BalancedDropSystem.eigenpath line 193
  47. lemma OAI.KirchbergRordam.BalancedDropSystem.lower_zero line 196
  48. lemma OAI.KirchbergRordam.BalancedDropSystem.lower_one line 200
  49. lemma OAI.KirchbergRordam.BalancedDropSystem.upper_zero line 204
  50. lemma OAI.KirchbergRordam.BalancedDropSystem.upper_one line 208
  51. lemma OAI.KirchbergRordam.BalancedDropSystem.eigen_cover line 213
  52. def OAI.KirchbergRordam.BalancedDropSystem.fiberMap line 226
  53. def OAI.KirchbergRordam.BalancedDropSystem.rawStep line 233
  54. lemma OAI.KirchbergRordam.BalancedDropSystem.rawStep_apply line 245
  55. lemma OAI.KirchbergRordam.BalancedDropSystem.zero_eval line 249
  56. lemma OAI.KirchbergRordam.BalancedDropSystem.one_eval line 258
  57. lemma OAI.KirchbergRordam.BalancedDropSystem.rawStep_zero line 270
  58. lemma OAI.KirchbergRordam.BalancedDropSystem.rawStep_one line 280
  59. def OAI.KirchbergRordam.BalancedDropSystem.step line 291
  60. lemma OAI.KirchbergRordam.BalancedDropSystem.rawStep_injective line 304
  61. lemma OAI.KirchbergRordam.BalancedDropSystem.step_injective line 312
  62. lemma OAI.KirchbergRordam.BalancedDropSystem.step_norm line 317