OAI/Analysis/MarkovType/FinitePowerIntegrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.lowerPowerKernel line 9
2. def OAI.MarkovSuperreflexivity.upperPowerKernel line 12
3. theorem OAI.MarkovSuperreflexivity.lowerPowerKernel_eq_indicator line 15
4. theorem OAI.MarkovSuperreflexivity.upperPowerKernel_eq_indicator line 21
5. theorem OAI.MarkovSuperreflexivity.integrable_lowerPowerKernel line 30
6. theorem OAI.MarkovSuperreflexivity.integral_lowerPowerKernel line 39
7. theorem OAI.MarkovSuperreflexivity.integrable_upperPowerKernel line 47
8. theorem OAI.MarkovSuperreflexivity.integral_upperPowerKernel line 56