OAI/Probability/SKRatio/Matrices/FiniteMax.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKRatioGaussian.interpolation_increment_identity line 52
  2. theorem OAI.SKRatioGaussian.interpolation_derivative_nonneg line 68
  3. theorem OAI.SKRatioGaussian.gaussian_smoothMax_comparison line 91
  4. def OAI.SKRatioGaussian.finiteMax line 115
  5. theorem OAI.SKRatioGaussian.le_finiteMax line 117
  6. theorem OAI.SKRatioGaussian.finiteMax_le line 120
  7. theorem OAI.SKRatioGaussian.continuous_finiteMax line 123
  8. theorem OAI.SKRatioGaussian.finiteMax_norm_le line 126
  9. theorem OAI.SKRatioGaussian.integrable_affineProcess line 133
  10. theorem OAI.SKRatioGaussian.integrable_finiteMax_affine line 138
  11. theorem OAI.SKRatioGaussian.integrable_smoothMax_affine line 144
  12. theorem OAI.SKRatioGaussian.gaussian_finiteMax_comparison line 151
  13. def OAI.SKRatioGaussian.supProcess line 191
  14. theorem OAI.SKRatioGaussian.continuous_affine_index line 195
  15. theorem OAI.SKRatioGaussian.supProcess_attained line 200
  16. theorem OAI.SKRatioGaussian.affine_le_supProcess line 208
  17. theorem OAI.SKRatioGaussian.supProcess_le line 215
  18. theorem OAI.SKRatioGaussian.continuous_supProcess line 223
  19. theorem OAI.SKRatioGaussian.affineProcess_abs_le line 233
  20. theorem OAI.SKRatioGaussian.integrable_supProcess line 246
  21. theorem OAI.SKRatioGaussian.exists_finite_affine_net line 265
  22. theorem OAI.SKRatioGaussian.affineProcess_difference_abs_le line 294
  23. theorem OAI.SKRatioGaussian.gaussian_supProcess_comparison line 313