OAI/Geometry/CAT0Fillings/Mass/Approximation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CAT0Fillings.BorelCoefficients.exists_measurable_coefficient_density line 16
2. theorem OAI.CAT0Fillings.BorelCoefficients.exists_mass_spectrum line 36
3. lemma OAI.CAT0Fillings.BorelCoefficients.abs_div_sub_div_le line 109
4. def OAI.CAT0Fillings.BorelCoefficients.coefficientScale line 128
5. def OAI.CAT0Fillings.BorelCoefficients.normalizeCoefficients line 129
6. lemma OAI.CAT0Fillings.BorelCoefficients.coefficientScale_one_le line 131
7. lemma OAI.CAT0Fillings.BorelCoefficients.abs_le_coefficientScale line 132
8. lemma OAI.CAT0Fillings.BorelCoefficients.normalizeCoefficients_budget line 134
9. lemma OAI.CAT0Fillings.BorelCoefficients.normalizeCoefficients_fixed line 138
10. lemma OAI.CAT0Fillings.BorelCoefficients.abs_coefficientScale_sub_le line 143
11. lemma OAI.CAT0Fillings.BorelCoefficients.normalizeCoefficients_dist_le line 153
12. lemma OAI.CAT0Fillings.BorelCoefficients.normalizeCoefficients_boundedLip line 162
13. lemma OAI.CAT0Fillings.BorelCoefficients.exists_lip_l1_approx line 182
14. theorem OAI.CAT0Fillings.BorelCoefficients.exists_admissible_coefficient_approx line 196