OAI/Geometry/CAT0Fillings/Mass/TestDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.integrable_gradient_weight line 18
2. lemma OAI.CAT0Fillings.ChartGeometry.chart_action_le_gradient line 27
3. lemma OAI.CAT0Fillings.ChartGeometry.action_le_gradient line 51
4. theorem OAI.CAT0Fillings.ChartGeometry.list_action_le_gradient line 66
5. lemma OAI.CAT0Fillings.BorelCoefficients.integrable_l2 line 102
6. lemma OAI.CAT0Fillings.BorelCoefficients.integral_abs_le_l2 line 105
7. def OAI.CAT0Fillings.BorelCoefficients.l2ToL1Linear line 127
8. def OAI.CAT0Fillings.BorelCoefficients.l2ToL1 line 144
9. lemma OAI.CAT0Fillings.BorelCoefficients.l2ToL1_coe line 151
10. theorem OAI.CAT0Fillings.BorelCoefficients.exists_coefficient_density line 156