OAI/Probability/SKRatio/Matrices/ExpSum.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SKRatioGaussian.(instance at line 50) line 50
  2. def OAI.SKRatioGaussian.expSum line 56
  3. def OAI.SKRatioGaussian.softWeight line 57
  4. def OAI.SKRatioGaussian.smoothMax line 58
  5. theorem OAI.SKRatioGaussian.expSum_pos line 60
  6. theorem OAI.SKRatioGaussian.softWeight_pos line 63
  7. theorem OAI.SKRatioGaussian.sum_softWeight line 66
  8. theorem OAI.SKRatioGaussian.softWeight_le_one line 70
  9. theorem OAI.SKRatioGaussian.continuous_softWeight line 74
  10. theorem OAI.SKRatioGaussian.continuous_smoothMax line 80
  11. theorem OAI.SKRatioGaussian.hasDerivAt_expSum line 86
  12. theorem OAI.SKRatioGaussian.hasDerivAt_smoothMax line 92
  13. theorem OAI.SKRatioGaussian.hasDerivAt_softWeight line 108
  14. theorem OAI.SKRatioGaussian.weighted_abs_le line 126
  15. theorem OAI.SKRatioGaussian.smoothMax_ge line 137
  16. theorem OAI.SKRatioGaussian.smoothMax_le line 145
  17. def OAI.SKRatioGaussian.affineProcess line 159
  18. theorem OAI.SKRatioGaussian.continuous_affineProcess line 163
  19. theorem OAI.SKRatioGaussian.affineProcess_coordinate_hasDerivAt line 170
  20. theorem OAI.SKRatioGaussian.affine_softWeight_coordinate_IBP line 182
  21. theorem OAI.SKRatioGaussian.weighted_covariance_identity line 208
  22. theorem OAI.SKRatioGaussian.smoothMax_norm_le line 219
  23. def OAI.SKRatioGaussian.interpolatedCoeff line 234
  24. def OAI.SKRatioGaussian.interpolatedCoeffDeriv line 237
  25. def OAI.SKRatioGaussian.processBound line 240
  26. theorem OAI.SKRatioGaussian.interpolatedCoeff_abs_le line 244
  27. theorem OAI.SKRatioGaussian.interpolatedCoeffDeriv_abs_le line 256
  28. theorem OAI.SKRatioGaussian.integrable_processBound line 268
  29. theorem OAI.SKRatioGaussian.interpolated_affine_hasDerivAt line 277
  30. def OAI.SKRatioGaussian.interpolationDerivative line 289
  31. theorem OAI.SKRatioGaussian.interpolationDerivative_norm_le line 294
  32. theorem OAI.SKRatioGaussian.interpolated_smoothMax_norm_le line 309
  33. theorem OAI.SKRatioGaussian.interpolation_hasDerivAt line 326
  34. theorem OAI.SKRatioGaussian.integrable_affine_weight line 356
  35. theorem OAI.SKRatioGaussian.integrable_coordinate_weight line 364
  36. theorem OAI.SKRatioGaussian.integrable_weight_covariance line 374
  37. theorem OAI.SKRatioGaussian.weighted_matrix_covariance_identity line 394
  38. theorem OAI.SKRatioGaussian.gaussian_linear_weight_IBP line 425