OAI/Probability/SKValue/Equations/GradientErrorConstant.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValue.gaussian_mesh_bound_linear line 17
  2. def OAI.SKValue.gradientErrorConstant line 30
  3. lemma OAI.SKValue.gradientMeshError_bound_linear line 34
  4. theorem OAI.SKValue.gradientMeshError_tendsto_zero line 44
  5. lemma OAI.SKValue.continuous_cdf_of_nullSingleton line 62
  6. lemma OAI.SKValue.strictMono_gaussian_cdf line 76
  7. lemma OAI.SKValue.cdf_mem_Ioo_of_strictMono line 88
  8. lemma OAI.SKValue.exists_cdf_eq line 94
  9. lemma OAI.SKValue.cdf_hasLaw_uniform line 100
  10. lemma OAI.SKValue.standardGaussian_cdf_hasLaw_uniform line 140
  11. lemma OAI.SKValue.measurable_real_sign line 145
  12. lemma OAI.SKValue.abs_real_sign_le_one line 150
  13. lemma OAI.SKValue.uniform_rounding_mean line 153
  14. lemma OAI.SKValue.gaussian_rounding_mean line 181
  15. lemma OAI.SKValue.product_rounding_integral line 188
  16. lemma OAI.SKValue.independent_rounding_integral line 210