OAI/Analysis/MarkovType/OrderedBoundedCubes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.C00.pairLinear line 19
  2. def OAI.MarkovSuperreflexivity.C00.collapseAtPair line 26
  3. theorem OAI.MarkovSuperreflexivity.C00.collapseAtPair_monotone line 28
  4. theorem OAI.MarkovSuperreflexivity.C00.mapDomain_pair_collapse line 33
  5. theorem OAI.MarkovSuperreflexivity.C00.mapDomain_pairLinear line 53
  6. theorem OAI.MarkovSuperreflexivity.OrderedNorm.subset_pairs_norm line 72
  7. theorem OAI.MarkovSuperreflexivity.OrderedNorm.pairLinear_sign_bound line 100
  8. theorem OAI.MarkovSuperreflexivity.OrderedNorm.pairLinear_upper line 127
  9. theorem OAI.MarkovSuperreflexivity.OrderedNorm.pairLinear_coordinate_lower line 135
  10. theorem OAI.MarkovSuperreflexivity.OrderedNorm.pairLinear_lower line 143
  11. theorem OAI.MarkovSuperreflexivity.OrderedNorm.exists_uniform_cubes_of_bounded_alternating line 154