OAI/Analysis/MarkovType/FiniteBoundedEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.sum_Icc_one_eq_sum_range_succ line 20
2. theorem OAI.MarkovSuperreflexivity.selectionCount_eq_card_filter_Icc line 27
3. theorem OAI.MarkovSuperreflexivity.finiteUpperL2_band_bound line 51
4. def OAI.MarkovSuperreflexivity.boundedEnergyConstant line 104
5. theorem OAI.MarkovSuperreflexivity.boundedEnergyConstant_nonneg line 107
6. theorem OAI.MarkovSuperreflexivity.finite_band_decomposition line 114
7. theorem OAI.MarkovSuperreflexivity.finiteUpperL2_bounded_energy line 152