OAI/Geometry/CAT0Fillings/Slices/BorelAction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.BorelCoefficients.integrable_bounded_measurable line 19
2. lemma OAI.CAT0Fillings.BorelCoefficients.borelAction_tendsto_of_bounded_pointwise line 25
3. def OAI.CAT0Fillings.BorelCoefficients.currentBorelAction line 47
4. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_eq line 51
5. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_eq_action line 56
6. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_bound line 62
7. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_tendsto line 76
8. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_add line 91
9. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_sub line 102
10. lemma OAI.CAT0Fillings.BorelCoefficients.currentBorelAction_smul line 113
11. lemma OAI.CAT0Fillings.BorelCoefficients.exists_lipschitz_closed_indicator_approximation line 122
12. def OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement line 171
13. lemma OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement.of_bounded_pointwise line 176
14. lemma OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement.add line 209
15. lemma OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement.sub line 224
16. lemma OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement.smul line 239
17. theorem OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement.indicator line 251
18. theorem OAI.CAT0Fillings.BorelCoefficients.ActionIntegralAgreement.bounded_measurable line 317