OAI/Analysis/MarkovType/RenormingBasic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MarkovSuperreflexivity.EquivalentNorm line 13

    Also declared: ComparatorChallenges/MarkovType.lean:48 (same declaration text).

  2. theorem OAI.MarkovSuperreflexivity.EquivalentNorm.eq_zero_iff line 26
  3. def OAI.MarkovSuperreflexivity.EquivalentNorm.original line 36
  4. theorem OAI.MarkovSuperreflexivity.EquivalentNorm.original_apply line 45
  5. def OAI.MarkovSuperreflexivity.UniformConvex line 49

    Also declared: ComparatorChallenges/MarkovType.lean:59 (same declaration text).

  6. def OAI.MarkovSuperreflexivity.UniformSmooth line 54
  7. def OAI.MarkovSuperreflexivity.HasEquivalentUCNorm line 59

    Also declared: ComparatorChallenges/MarkovType.lean:64 (same declaration text).

  8. def OAI.MarkovSuperreflexivity.HasEquivalentUSNorm line 62
  9. theorem OAI.MarkovSuperreflexivity.uniformConvex_of_subsingleton line 65
  10. theorem OAI.MarkovSuperreflexivity.uniformSmooth_of_subsingleton line 74
  11. theorem OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_subsingleton line 83
  12. theorem OAI.MarkovSuperreflexivity.hasEquivalentUSNorm_of_subsingleton line 86