OAI/Geometry/CAT0Fillings/Mass/Convolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CAT0Fillings.BorelCoefficients.CoefficientList line 16
2. instance OAI.CAT0Fillings.BorelCoefficients.coefficientList_nonempty line 19
3. lemma OAI.CAT0Fillings.BorelCoefficients.coefficientList_eval_continuous line 25
4. lemma OAI.CAT0Fillings.BorelCoefficients.finite_list_le_mass line 39
5. theorem OAI.CAT0Fillings.BorelCoefficients.exists_countable_mass_lists line 55
6. theorem OAI.CAT0Fillings.BorelCoefficients.ae_mass_le_of_listwise line 83
7. lemma OAI.CAT0Fillings.SmoothCutoff.dprofile_integrable_measure line 109
8. theorem OAI.CAT0Fillings.SmoothCutoff.ae_tendsto_dprofile_measure line 115