OAI/Geometry/WeakHessian/Measure/DecayCutoffLp.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.integral_mul_le_weighted line 50
2. lemma OAI.WeakHessian.memLp_decayCutoff line 75
3. def OAI.WeakHessian.decayCutoffLp line 84
4. lemma OAI.WeakHessian.decayCutoffLp_norm_tendsto line 89
5. lemma OAI.WeakHessian.integral_cutoff_error_le_weighted line 108
6. lemma OAI.WeakHessian.integral_tendsto_of_weighted_bound line 127