OAI/Probability/GaussianPropeller/CapNumeric.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.CapNumeric.Q line 37
  2. def OAI.GaussianPropeller.CapNumeric.U line 38
  3. def OAI.GaussianPropeller.CapNumeric.R line 39
  4. lemma OAI.GaussianPropeller.CapNumeric.hasDerivAt_Q line 41
  5. lemma OAI.GaussianPropeller.CapNumeric.hasDerivAt_R line 45
  6. lemma OAI.GaussianPropeller.CapNumeric.hasDerivAt_U line 50
  7. lemma OAI.GaussianPropeller.CapNumeric.Q_nonneg line 57
  8. lemma OAI.GaussianPropeller.CapNumeric.Q_antitone line 60
  9. lemma OAI.GaussianPropeller.CapNumeric.R_antitone line 67
  10. lemma OAI.GaussianPropeller.CapNumeric.U_middle line 76
  11. lemma OAI.GaussianPropeller.CapNumeric.U_bound line 88
  12. lemma OAI.GaussianPropeller.Cap.integral_u_sqrt line 119
  13. def OAI.GaussianPropeller.Cap.sphereGap line 134
  14. lemma OAI.GaussianPropeller.Cap.sphereGap_eq line 136
  15. lemma OAI.GaussianPropeller.Cap.sqrt_two_upper line 146
  16. lemma OAI.GaussianPropeller.Cap.hasDerivAt_sqrt_two line 156
  17. def OAI.GaussianPropeller.Cap.gapPrim line 162
  18. lemma OAI.GaussianPropeller.Cap.hasDerivAt_gapPrim line 165
  19. lemma OAI.GaussianPropeller.Cap.sphereGap_upper line 174
  20. lemma OAI.GaussianPropeller.Cap.cone_four line 205