OAI/Geometry/WeakHessian/Sobolev/CompContDiff2.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.LocalSobolev.comp_contDiff line 50
2. lemma OAI.WeakHessian.weakGradient_comp_contDiff_le line 57
3. lemma OAI.WeakHessian.gamma_chain_residual line 64
4. lemma OAI.WeakHessian.gamma_comp_contDiff line 93
5. lemma OAI.WeakHessian.LocalSobolev.exp_bounded line 112
6. lemma OAI.WeakHessian.gamma_exp_left line 122
7. lemma OAI.WeakHessian.weakGradient_exp_bound line 133
8. lemma OAI.WeakHessian.gamma_mul_exp_left line 144
9. lemma OAI.WeakHessian.memLp_gamma_of_lipschitz line 157