OAI/Geometry/CAT0Fillings/Gradient/Pairing.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.ChartGeometry.testWeight line 17
2. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_testWeight line 22
3. lemma OAI.CAT0Fillings.ChartGeometry.ae_testWeight_bound line 42
4. lemma OAI.CAT0Fillings.ChartGeometry.memLp_testWeight line 63
5. lemma OAI.CAT0Fillings.ChartGeometry.testWeight_sub line 70
6. lemma OAI.CAT0Fillings.ChartGeometry.integrable_testWeight_mul line 75
7. lemma OAI.CAT0Fillings.ChartGeometry.testWeight_gradient line 86
8. lemma OAI.CAT0Fillings.integral_norm_le_lpNorm_two line 135
9. lemma OAI.CAT0Fillings.lpNorm_Lp line 147
10. def OAI.CAT0Fillings.ChartGeometry.pairing line 156
11. lemma OAI.CAT0Fillings.ChartGeometry.pairing_sub line 160
12. lemma OAI.CAT0Fillings.ChartGeometry.abs_pairing_le line 178
13. lemma OAI.CAT0Fillings.ChartGeometry.continuous_pairing line 203
14. lemma OAI.CAT0Fillings.ChartGeometry.pairing_gradient line 215