OAI/Analysis/MarkovType/EndNorm.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.C00.endpointAlternating line 17
  2. def OAI.MarkovSuperreflexivity.C00.collapseTail line 20
  3. theorem OAI.MarkovSuperreflexivity.C00.collapseTail_monotone line 22
  4. theorem OAI.MarkovSuperreflexivity.C00.mapDomain_collapseTail_endpointAlternating line 27
  5. theorem OAI.MarkovSuperreflexivity.C00.endpointAlternating_supportedBelow line 45
  6. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_shift_alternating_odd line 56
  7. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_shift_alternating_even line 65
  8. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_endpointAlternating_odd line 79
  9. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_endpointAlternating_even line 87
  10. theorem OAI.MarkovSuperreflexivity.C00.prefixCut_endpointAlternating_last line 95
  11. theorem OAI.MarkovSuperreflexivity.OrderedNorm.endpoint_error_le line 114
  12. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_le_twice_endpoint line 123
  13. theorem OAI.MarkovSuperreflexivity.OrderedNorm.endpointAlternating_le_of_prefixes line 142
  14. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_six_le_of_prefixes line 162
  15. theorem OAI.MarkovSuperreflexivity.OrderedNorm.alternatingNorm_six_le_of_levels line 175