OAI/Probability/SKGap/Localization/ExpSum.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SKGap.(instance at line 49) line 49
  2. def OAI.SKGap.expSum line 55
  3. def OAI.SKGap.softWeight line 56
  4. def OAI.SKGap.smoothMax line 57
  5. theorem OAI.SKGap.expSum_pos line 59
  6. theorem OAI.SKGap.softWeight_pos line 62
  7. theorem OAI.SKGap.sum_softWeight line 65
  8. theorem OAI.SKGap.softWeight_le_one line 69
  9. theorem OAI.SKGap.continuous_softWeight line 73
  10. theorem OAI.SKGap.continuous_smoothMax line 79
  11. theorem OAI.SKGap.hasDerivAt_expSum line 85
  12. theorem OAI.SKGap.hasDerivAt_smoothMax line 91
  13. theorem OAI.SKGap.hasDerivAt_softWeight line 107
  14. theorem OAI.SKGap.weighted_abs_le line 125
  15. theorem OAI.SKGap.smoothMax_ge line 136
  16. theorem OAI.SKGap.smoothMax_le line 144
  17. def OAI.SKGap.affineProcess line 158
  18. theorem OAI.SKGap.continuous_affineProcess line 162
  19. theorem OAI.SKGap.affineProcess_coordinate_hasDerivAt line 169
  20. theorem OAI.SKGap.affine_softWeight_coordinate_IBP line 181
  21. theorem OAI.SKGap.weighted_covariance_identity line 207
  22. theorem OAI.SKGap.smoothMax_norm_le line 218
  23. def OAI.SKGap.interpolatedCoeff line 233
  24. def OAI.SKGap.interpolatedCoeffDeriv line 236
  25. def OAI.SKGap.processBound line 239
  26. theorem OAI.SKGap.interpolatedCoeff_abs_le line 243
  27. theorem OAI.SKGap.interpolatedCoeffDeriv_abs_le line 255
  28. theorem OAI.SKGap.integrable_processBound line 267
  29. theorem OAI.SKGap.interpolated_affine_hasDerivAt line 276
  30. def OAI.SKGap.interpolationDerivative line 288
  31. theorem OAI.SKGap.interpolationDerivative_norm_le line 293
  32. theorem OAI.SKGap.interpolated_smoothMax_norm_le line 308
  33. theorem OAI.SKGap.interpolation_hasDerivAt line 325
  34. theorem OAI.SKGap.integrable_affine_weight line 355
  35. theorem OAI.SKGap.integrable_coordinate_weight line 363
  36. theorem OAI.SKGap.integrable_weight_covariance line 373
  37. theorem OAI.SKGap.weighted_matrix_covariance_identity line 393
  38. theorem OAI.SKGap.gaussian_linear_weight_IBP line 424