OAI/Geometry/IntegralFillings/Slicing/NormalRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.Slicing.controls_from_bounded_measures line 36
2. lemma OAI.SharpIntegralFillings.Slicing.profile_comp_boundedLip line 58
3. lemma OAI.SharpIntegralFillings.Slicing.dprofile_comp_boundedLip line 68
4. lemma OAI.SharpIntegralFillings.Slicing.profile_L1_tendsto line 75
5. lemma OAI.SharpIntegralFillings.Slicing.profile_boundary_tendsto line 106
6. theorem OAI.SharpIntegralFillings.Slicing.ae_finite_boundary_restrict_cycle line 123
7. theorem OAI.SharpIntegralFillings.Slicing.ae_normal_restrict_cycle line 161