OAI/Probability/SKRatio/Matrices/LipschitzNormedConvolution.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKRatioGaussian.lipschitz_normed_convolution line 30
  2. theorem OAI.SKRatioGaussian.exists_smooth_lipschitz_approx line 54
  3. theorem OAI.SKRatioGaussian.gaussian_integrable_exp_norm line 77
  4. theorem OAI.SKRatioGaussian.stdGaussian_map_dual line 96
  5. theorem OAI.SKRatioGaussian.stdGaussian_integrable_exp_dual line 101
  6. theorem OAI.SKRatioGaussian.stdGaussian_integral_exp_dual line 108
  7. theorem OAI.SKRatioGaussian.gaussian_integrable_exp_lipschitz line 114
  8. theorem OAI.SKRatioGaussian.gaussian_integrable_lipschitz line 136
  9. theorem OAI.SKRatioGaussian.exp_interval_average_le line 151
  10. theorem OAI.SKRatioGaussian.rotation_snd_norm_le line 170
  11. theorem OAI.SKRatioGaussian.hasDerivAt_rotation_fst line 181
  12. theorem OAI.SKRatioGaussian.rotation_fundamental_theorem line 187
  13. theorem OAI.SKRatioGaussian.rotation_exp_difference_le line 203
  14. theorem OAI.SKRatioGaussian.exp_dual_le line 218
  15. theorem OAI.SKRatioGaussian.rotation_exp_dual_le line 228
  16. theorem OAI.SKRatioGaussian.stdGaussian_integrable_variable_dual line 245
  17. theorem OAI.SKRatioGaussian.stdGaussian_integral_variable_dual_le line 255
  18. theorem OAI.SKRatioGaussian.stdGaussian_integral_rotation_variable_dual_le line 273
  19. theorem OAI.SKRatioGaussian.stdGaussian_integrable_rotation_variable_dual line 283
  20. theorem OAI.SKRatioGaussian.lipschitz_of_bounded_derivative line 299
  21. lemma OAI.SKRatioGaussian.exp_mul_sub line 307
  22. theorem OAI.SKRatioGaussian.stdGaussian_integrable_exp_difference line 312
  23. theorem OAI.SKRatioGaussian.stdGaussian_mgf_difference_le line 320
  24. theorem OAI.SKRatioGaussian.stdGaussian_mgf_centered_le line 357
  25. theorem OAI.SKRatioGaussian.centered_mgf_le_of_uniform_dist line 391