OAI/Probability/SKGap/Localization/Reference.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.GaussianStep.reference line 12
  2. instance OAI.SKGap.GaussianStep.reference_probability line 15
  3. lemma OAI.SKGap.GaussianStep.integrable_exp_linear line 18
  4. lemma OAI.SKGap.GaussianStep.integral_exp_linear line 23
  5. structure OAI.SKGap.GaussianStep.Prior line 33
  6. lemma OAI.SKGap.GaussianStep.Prior.ext line 38
  7. instance OAI.SKGap.GaussianStep.(instance at line 43) line 43
  8. def OAI.SKGap.GaussianStep.gibbsPrior line 45
  9. def OAI.SKGap.GaussianStep.mean line 48
  10. def OAI.SKGap.GaussianStep.likelihood line 50
  11. def OAI.SKGap.GaussianStep.density line 53
  12. lemma OAI.SKGap.GaussianStep.likelihood_pos line 56
  13. lemma OAI.SKGap.GaussianStep.integrable_likelihood line 59
  14. lemma OAI.SKGap.GaussianStep.integral_likelihood line 68
  15. lemma OAI.SKGap.GaussianStep.density_jensen line 80
  16. lemma OAI.SKGap.GaussianStep.density_pos line 99
  17. lemma OAI.SKGap.GaussianStep.integrable_density line 102
  18. lemma OAI.SKGap.GaussianStep.integral_density line 106
  19. lemma OAI.SKGap.GaussianStep.mean_abs_le_one line 113
  20. def OAI.SKGap.GaussianStep.interaction line 124
  21. lemma OAI.SKGap.GaussianStep.interaction_abs_le line 127
  22. lemma OAI.SKGap.GaussianStep.interaction_remainder_bound line 151
  23. lemma OAI.SKGap.GaussianStep.interaction_sum line 163
  24. lemma OAI.SKGap.GaussianStep.signed_sum_left line 175
  25. lemma OAI.SKGap.GaussianStep.signed_sum_right line 187
  26. lemma OAI.SKGap.GaussianStep.signed_sum_product line 197
  27. lemma OAI.SKGap.GaussianStep.signed_interaction line 206
  28. def OAI.SKGap.GaussianStep.pairKernel line 229
  29. lemma OAI.SKGap.GaussianStep.integrable_pairKernel line 232
  30. lemma OAI.SKGap.GaussianStep.integral_pairKernel line 240
  31. lemma OAI.SKGap.GaussianStep.likelihood_pair line 250
  32. def OAI.SKGap.GaussianStep.majorant line 260
  33. lemma OAI.SKGap.GaussianStep.majorant_eq_sum line 263
  34. lemma OAI.SKGap.GaussianStep.majorant_nonneg line 277
  35. lemma OAI.SKGap.GaussianStep.integrable_majorant line 280
  36. lemma OAI.SKGap.GaussianStep.integral_majorant line 287
  37. lemma OAI.SKGap.GaussianStep.interaction_exp_sum_bound line 297
  38. def OAI.SKGap.GaussianStep.quadraticIntegrand line 323
  39. lemma OAI.SKGap.GaussianStep.quadraticIntegrand_nonneg line 326
  40. lemma OAI.SKGap.GaussianStep.quadraticIntegrand_le_majorant line 329
  41. lemma OAI.SKGap.GaussianStep.continuous_likelihood line 338
  42. lemma OAI.SKGap.GaussianStep.continuous_density line 342
  43. lemma OAI.SKGap.GaussianStep.continuous_quadraticIntegrand line 346
  44. lemma OAI.SKGap.GaussianStep.integrable_quadraticIntegrand line 354
  45. theorem OAI.SKGap.GaussianStep.quadratic_bound line 361
  46. def OAI.SKGap.GaussianStep.avg line 373
  47. def OAI.SKGap.GaussianStep.var line 375
  48. def OAI.SKGap.GaussianStep.posterior line 378
  49. lemma OAI.SKGap.GaussianStep.var_nonneg line 386
  50. lemma OAI.SKGap.GaussianStep.avg_const line 389
  51. lemma OAI.SKGap.GaussianStep.avg_sub line 392
  52. lemma OAI.SKGap.GaussianStep.avg_mul_const line 396
  53. lemma OAI.SKGap.GaussianStep.avg_center line 400
  54. lemma OAI.SKGap.GaussianStep.avg_shift_square line 403