OAI/Probability/GaussianPropeller/Quantile.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GaussianPropeller.Quantile.φ line 21
  2. def OAI.GaussianPropeller.Quantile.Φ line 22
  3. lemma OAI.GaussianPropeller.Quantile.φ_pos line 24
  4. lemma OAI.GaussianPropeller.Quantile.φ_neg line 25
  5. lemma OAI.GaussianPropeller.Quantile.integrable_φ line 26
  6. lemma OAI.GaussianPropeller.Quantile.integral_φ line 31
  7. lemma OAI.GaussianPropeller.Quantile.hasDerivAt_φ line 38
  8. lemma OAI.GaussianPropeller.Quantile.continuous_φ line 43
  9. lemma OAI.GaussianPropeller.Quantile.hasDerivAt_Φ line 45
  10. lemma OAI.GaussianPropeller.Quantile.continuous_Φ line 55
  11. lemma OAI.GaussianPropeller.Quantile.strictMono_Φ line 57
  12. lemma OAI.GaussianPropeller.Quantile.Φ_pos line 59
  13. lemma OAI.GaussianPropeller.Quantile.Φ_eq_one_sub_tail line 63
  14. lemma OAI.GaussianPropeller.Quantile.Φ_neg line 68
  15. lemma OAI.GaussianPropeller.Quantile.Φ_lt_one line 74
  16. lemma OAI.GaussianPropeller.Quantile.Φ_mem line 78
  17. lemma OAI.GaussianPropeller.Quantile.Φ_zero line 79
  18. lemma OAI.GaussianPropeller.Quantile.tendsto_Φ_atTop line 83
  19. lemma OAI.GaussianPropeller.Quantile.tendsto_Φ_atBot line 88
  20. lemma OAI.GaussianPropeller.Quantile.range_Φ line 92
  21. def OAI.GaussianPropeller.Quantile.cdfIso line 100
  22. lemma OAI.GaussianPropeller.Quantile.cdfIso_coe line 102
  23. def OAI.GaussianPropeller.Quantile.q line 103
  24. lemma OAI.GaussianPropeller.Quantile.q_of_mem line 105
  25. lemma OAI.GaussianPropeller.Quantile.Φ_q line 107
  26. lemma OAI.GaussianPropeller.Quantile.q_Φ line 110
  27. lemma OAI.GaussianPropeller.Quantile.continuousOn_q line 113
  28. lemma OAI.GaussianPropeller.Quantile.continuousAt_q line 121
  29. lemma OAI.GaussianPropeller.Quantile.hasDerivAt_q line 123
  30. lemma OAI.GaussianPropeller.Quantile.strictMonoOn_q line 129
  31. def OAI.GaussianPropeller.Quantile.I line 134
  32. lemma OAI.GaussianPropeller.Quantile.I_pos line 135
  33. lemma OAI.GaussianPropeller.Quantile.I_Φ line 136
  34. lemma OAI.GaussianPropeller.Quantile.hasDerivAt_I line 137
  35. lemma OAI.GaussianPropeller.Quantile.antitoneOn_I_deriv line 140
  36. lemma OAI.GaussianPropeller.Quantile.concaveOn_I line 143
  37. lemma OAI.GaussianPropeller.Quantile.concave_le_tangent line 152
  38. lemma OAI.GaussianPropeller.Quantile.I_le_tangent line 166
  39. lemma OAI.GaussianPropeller.Quantile.φ_le_zero line 170
  40. lemma OAI.GaussianPropeller.Quantile.integrable_Φ_comp line 178
  41. lemma OAI.GaussianPropeller.Quantile.integrable_φ_comp line 184
  42. lemma OAI.GaussianPropeller.Quantile.integral_Φ_mem line 190
  43. lemma OAI.GaussianPropeller.Quantile.integral_φ_le_I line 204
  44. lemma OAI.GaussianPropeller.Quantile.hasDerivAt_integral_shift line 218
  45. lemma OAI.GaussianPropeller.Quantile.hasDerivAt_quantile_shift line 232
  46. lemma OAI.GaussianPropeller.Quantile.quantile_shift_le line 238