OAI/Geometry/CAT0Fillings/Jacobian/Mixed.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.mixedJacobian line 25
2. lemma OAI.CAT0Fillings.continuous_mixedJacobian line 31
3. lemma OAI.CAT0Fillings.mixedJacobian_eq_zero_of_fderiv_eq_zero line 45
4. lemma OAI.CAT0Fillings.hasCompactSupport_mixedJacobian line 53
5. lemma OAI.CAT0Fillings.mixedJacobian_mul line 62
6. lemma OAI.CAT0Fillings.integral_smooth_mixedJacobian_mul line 79
7. lemma OAI.CAT0Fillings.exists_mixedJacobian_bound line 98
8. lemma OAI.CAT0Fillings.aestronglyMeasurable_mixedJacobian line 117
9. lemma OAI.CAT0Fillings.ae_tendsto_mixedJacobian line 126
10. lemma OAI.CAT0Fillings.tendsto_integral_weighted_mixedJacobian line 144
11. lemma OAI.CAT0Fillings.uniformly_bounded_lipschitz_on_compact line 168