OAI/Geometry/WeakHessian/Entropy/RenyiKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.renyiKernel line 46
  2. lemma OAI.WeakHessian.renyiKernel_nonneg line 48
  3. lemma OAI.WeakHessian.rpow_sub_le_add_one line 58
  4. lemma OAI.WeakHessian.tendsto_renyiKernel line 65
  5. lemma OAI.WeakHessian.continuous_renyiKernel line 86
  6. lemma OAI.WeakHessian.renyiKernel_large_dimension line 90
  7. lemma OAI.WeakHessian.renyiKernel_le_klFun line 102
  8. lemma OAI.WeakHessian.integrable_rpow_sub line 118
  9. lemma OAI.WeakHessian.integrable_renyiKernel line 127
  10. lemma OAI.WeakHessian.tendsto_integral_rpow_sub line 132
  11. lemma OAI.WeakHessian.integral_klFun_le_of_renyi_bounds line 148
  12. lemma OAI.WeakHessian.tendsto_integral_renyiKernel line 189