OAI/Analysis/MarkovType/JamesCubeImprovement.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.CoordinateCopies line 19
  2. def OAI.MarkovSuperreflexivity.cubeBlock line 24
  3. lemma OAI.MarkovSuperreflexivity.cubeBlock_single line 34
  4. def OAI.MarkovSuperreflexivity.cubeBlend line 45
  5. lemma OAI.MarkovSuperreflexivity.cubeBlend_single line 57
  6. lemma OAI.MarkovSuperreflexivity.norm_cubeBlend_le line 65
  7. lemma OAI.MarkovSuperreflexivity.exists_cube_gain line 80
  8. lemma OAI.MarkovSuperreflexivity.coordinateCopies_amplify line 122
  9. lemma OAI.MarkovSuperreflexivity.exists_coordinate_improvement line 149
  10. lemma OAI.MarkovSuperreflexivity.cube_lower_of_coordinate_bounds line 171
  11. theorem OAI.MarkovSuperreflexivity.james_cube_improvement line 211