OAI/Analysis/MarkovType/OrderedJColumns.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.range_cut_add_shift line 16
  2. def OAI.MarkovSuperreflexivity.C00.jColumn line 56
  3. theorem OAI.MarkovSuperreflexivity.C00.jColumn_add_period line 59
  4. theorem OAI.MarkovSuperreflexivity.C00.shift_jColumn line 79
  5. theorem OAI.MarkovSuperreflexivity.C00.cutSum_jColumn_add_shift line 92
  6. theorem OAI.MarkovSuperreflexivity.C00.sum_jColumn line 109
  7. theorem OAI.MarkovSuperreflexivity.OrderedNorm.finite_sum_le line 136
  8. theorem OAI.MarkovSuperreflexivity.OrderedNorm.shift_norm line 145
  9. theorem OAI.MarkovSuperreflexivity.OrderedNorm.basis_norm line 151
  10. theorem OAI.MarkovSuperreflexivity.OrderedNorm.jColumn_norm line 154
  11. theorem OAI.MarkovSuperreflexivity.OrderedNorm.jColumn_cut_lower line 168
  12. theorem OAI.MarkovSuperreflexivity.OrderedNorm.exists_unit_jColumns_of_unbounded line 214