OAI/Geometry/CAT0Fillings/BV/WeakCalculus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.IntegerChart.linear_pi_expansion line 14
2. lemma OAI.CAT0Fillings.IntegerChart.ae_fderivWithin_scalar_multi line 23
3. lemma OAI.CAT0Fillings.IntegerChart.ae_jacobian_update_multi line 43
4. lemma OAI.CAT0Fillings.Foundations.IntegerRectifiable.apply_update_multi line 73
5. lemma OAI.CAT0Fillings.Slicing.NormalApprox.product_rule line 110
6. lemma OAI.CAT0Fillings.Slicing.NormalApprox.apply_update_multi line 124
7. lemma OAI.CAT0Fillings.Slicing.NormalApprox.apply_permute line 159
8. lemma OAI.CAT0Fillings.Slicing.NormalApprox.abs_apply_permute line 175
9. lemma OAI.CAT0Fillings.Slicing.NormalApprox.head_measure_bound line 181
10. lemma OAI.CAT0Fillings.Slicing.NormalApprox.coordinate_measure_bound line 212
11. theorem OAI.CAT0Fillings.Slicing.fullSlice_distributional_bound line 240