OAI/Probability/SKValue/Equations/BetaBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.inv_sqrt_eq_rpow line 12
  2. lemma OAI.SKValue.intervalIntegrable_inv_sqrt line 15
  3. lemma OAI.SKValue.integral_inv_sqrt line 21
  4. lemma OAI.SKValue.intervalIntegrable_inv_sqrt_sub line 34
  5. lemma OAI.SKValue.intervalIntegrable_inv_sqrt_sub_left line 39
  6. lemma OAI.SKValue.integral_inv_sqrt_sub line 44
  7. lemma OAI.SKValue.integral_inv_sqrt_sub_left line 48
  8. def OAI.SKValue.sqrtKernel line 52
  9. def OAI.SKValue.sqrtMajorant line 53
  10. lemma OAI.SKValue.sqrtKernel_nonneg line 56
  11. lemma OAI.SKValue.sqrtKernel_le_majorant line 58
  12. lemma OAI.SKValue.sqrtMajorant_integrable line 94
  13. lemma OAI.SKValue.sqrtKernel_integrable line 98
  14. lemma OAI.SKValue.sqrtKernel_integral_le_eight line 108