OAI/Analysis/MarkovType/WalkDrift.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean line 22
  2. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.sum_word_snoc line 25
  3. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_nonneg line 34
  4. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_mono line 40
  5. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_add line 46
  6. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_const line 51
  7. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMass_sum line 63
  8. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_snoc line 68
  9. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.fixed_prefix_extension_sum line 73
  10. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.fixed_prefix_mass line 86
  11. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.list_ofFn_snoc line 95
  12. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_length_succ line 100
  13. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.uniformWordMean_length_ge line 126
  14. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.length_ofFn_le line 143
  15. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.weightedMean_length_ge_of_uniform_letters line 150
  16. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.reducedLength_uniform_mean_ge line 164
  17. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.reducedLength_ofFn_le line 170
  18. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.reducedLength_weighted_mean_ge line 174
  19. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.reducedLength_tail_all_good line 184