OAI/Probability/SKGap/Localization/FiniteMax.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGap.interpolation_increment_identity line 51
  2. theorem OAI.SKGap.interpolation_derivative_nonneg line 67
  3. theorem OAI.SKGap.gaussian_smoothMax_comparison line 90
  4. def OAI.SKGap.finiteMax line 114
  5. theorem OAI.SKGap.le_finiteMax line 116
  6. theorem OAI.SKGap.finiteMax_le line 119
  7. theorem OAI.SKGap.continuous_finiteMax line 122
  8. theorem OAI.SKGap.finiteMax_norm_le line 125
  9. theorem OAI.SKGap.integrable_affineProcess line 132
  10. theorem OAI.SKGap.integrable_finiteMax_affine line 137
  11. theorem OAI.SKGap.integrable_smoothMax_affine line 143
  12. theorem OAI.SKGap.gaussian_finiteMax_comparison line 150
  13. def OAI.SKGap.supProcess line 190
  14. theorem OAI.SKGap.continuous_affine_index line 194
  15. theorem OAI.SKGap.supProcess_attained line 199
  16. theorem OAI.SKGap.affine_le_supProcess line 207
  17. theorem OAI.SKGap.supProcess_le line 214
  18. theorem OAI.SKGap.continuous_supProcess line 222
  19. theorem OAI.SKGap.affineProcess_abs_le line 232
  20. theorem OAI.SKGap.integrable_supProcess line 245
  21. theorem OAI.SKGap.exists_finite_affine_net line 264
  22. theorem OAI.SKGap.affineProcess_difference_abs_le line 293
  23. theorem OAI.SKGap.gaussian_supProcess_comparison line 312