OAI/Analysis/MarkovType/WeightedEvents.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.eventMass line 17
2. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.weightedMean line 21
3. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.eventMass_nonneg line 23
4. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.eventMass_mono line 33
5. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.eventMass_exists_le_sum line 47
6. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.eventMass_sub_le_and_not line 73
7. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.eventMass_sub_sum_le_all_good line 92
8. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.weightedMean_le_quarter_add_tail line 107
9. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.quarter_le_eventMass_of_half_le_weightedMean line 128
10. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.quarter_sub_failure_le_tail_all_good line 137
11. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.three_twentieths_le_tail_all_good line 159