OAI/Probability/GaussianPropeller/CapBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.Cap.coneCap line 40
  2. lemma OAI.GaussianPropeller.Cap.measurableSet_coneCap line 43
  3. lemma OAI.GaussianPropeller.Cap.coneCap_smul line 46
  4. lemma OAI.GaussianPropeller.Cap.integrable_coord line 52
  5. lemma OAI.GaussianPropeller.Cap.tail_first_gaussian line 57
  6. lemma OAI.GaussianPropeller.Cap.integral_cap line 65
  7. lemma OAI.GaussianPropeller.Cap.moment_cap line 80
  8. lemma OAI.GaussianPropeller.Cap.integral_cone_norm line 96
  9. lemma OAI.GaussianPropeller.Cap.coneCap_criterion line 124
  10. lemma OAI.GaussianPropeller.Cap.moment_rearrange line 145
  11. lemma OAI.GaussianPropeller.Cap.cap_parameter line 185
  12. lemma OAI.GaussianPropeller.Cap.cone_three line 199
  13. lemma OAI.GaussianPropeller.Cap.capP_deriv_three line 225
  14. def OAI.GaussianPropeller.Cap.sphereTail line 241
  15. lemma OAI.GaussianPropeller.Cap.sphereTail_zero line 243
  16. lemma OAI.GaussianPropeller.Cap.hasDerivAt_sphereTail line 255
  17. lemma OAI.GaussianPropeller.Cap.cap_parameter' line 261
  18. lemma OAI.GaussianPropeller.Cap.capP_three_sphere line 269