OAI/Probability/ParisiFinite/IntegrableExpField.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Integrable Exp Field.

  1. lemma OAI.SKCavity.integrable_exp_field line 65
  2. lemma OAI.SKCavity.integral_exp_field line 71
  3. def OAI.SKCavity.gaussianLogAverage line 85
  4. lemma OAI.SKCavity.integrable_gaussianLogAverage line 88
  5. lemma OAI.SKCavity.empirical_log_exp line 94
  6. lemma OAI.SKCavity.integrable_empirical_log_exp line 102
  7. def OAI.SKCavity.samplePressure line 108
  8. lemma OAI.SKCavity.integral_empirical_log_exp line 112
  9. lemma OAI.SKCavity.integrable_average_exp_field line 121
  10. lemma OAI.SKCavity.integral_average_exp_field_le line 125
  11. theorem OAI.SKCavity.gaussian_sample_error line 142
  12. def OAI.SKCavity.overlapMatrix line 190
  13. lemma OAI.SKCavity.gramBlock_posSemidef line 192
  14. lemma OAI.SKCavity.exists_gramFactor line 211
  15. def OAI.SKCavity.gramFactor line 218
  16. lemma OAI.SKCavity.kernel_gramFactor line 221
  17. lemma OAI.SKCavity.gramFactor_diag line 224
  18. def OAI.SKCavity.gramPressure line 229
  19. lemma OAI.SKCavity.gramPressure_eq line 232
  20. lemma OAI.SKCavity.gramEntry_dist line 244
  21. lemma OAI.SKCavity.gramPressure_lipschitz_bound line 249
  22. lemma OAI.SKCavity.continuous_gramPressure line 266
  23. def OAI.SKCavity.signBool line 283
  24. lemma OAI.SKCavity.signBool_sq line 285
  25. def OAI.SKCavity.doubled line 287
  26. lemma OAI.SKCavity.partition_doubled line 290
  27. lemma OAI.SKCavity.log_average_cosh line 299
  28. def OAI.SKCavity.gaussianCoshAverage line 307
  29. lemma OAI.SKCavity.integrable_gaussianCoshAverage line 310
  30. lemma OAI.SKCavity.empirical_log_cosh line 317
  31. lemma OAI.SKCavity.integrable_empirical_log_cosh line 331
  32. def OAI.SKCavity.sampleCoshPressure line 337
  33. lemma OAI.SKCavity.integral_empirical_log_cosh line 341
  34. lemma OAI.SKCavity.cosh_squared_bound line 355
  35. lemma OAI.SKCavity.cosh_inv_squared_bound line 362
  36. lemma OAI.SKCavity.average_cosh_squared_bound line 368
  37. lemma OAI.SKCavity.average_cosh_inverse_bound line 377
  38. theorem OAI.SKCavity.gaussian_cosh_sample_error line 384
  39. def OAI.SKCavity.coshGramCoeff line 434
  40. lemma OAI.SKCavity.kernel_coshGramCoeff line 437
  41. lemma OAI.SKCavity.diag_coshGramCoeff line 447
  42. def OAI.SKCavity.squareGramCoeff line 451
  43. lemma OAI.SKCavity.kernel_squareGramCoeff line 454
  44. lemma OAI.SKCavity.diag_squareGramCoeff line 466
  45. def OAI.SKCavity.coshGramPressure line 470
  46. def OAI.SKCavity.squareGramPressure line 473
  47. def OAI.SKCavity.cavityGramObservable line 476
  48. lemma OAI.SKCavity.abs_signBool line 479
  49. lemma OAI.SKCavity.cosh_kernel_dist line 481
  50. lemma OAI.SKCavity.coshGramPressure_lipschitz line 487
  51. lemma OAI.SKCavity.overlap_square_dist line 501
  52. lemma OAI.SKCavity.square_kernel_dist line 508
  53. lemma OAI.SKCavity.squareGramPressure_lipschitz line 516
  54. lemma OAI.SKCavity.continuous_coshGramPressure line 530
  55. lemma OAI.SKCavity.continuous_squareGramPressure line 538
  56. lemma OAI.SKCavity.continuous_cavityGramObservable line 546
  57. lemma OAI.SKCavity.integrable_field_prod line 561
  58. lemma OAI.SKCavity.expected_independent_integral line 566
  59. lemma OAI.SKCavity.integrable_logAverage_prod line 582
  60. lemma OAI.SKCavity.integrable_gaussianLogAverage_field line 590
  61. lemma OAI.SKCavity.integral_gaussianLogAverage line 594
  62. lemma OAI.SKCavity.integrable_coshAverage_prod line 607
  63. lemma OAI.SKCavity.integrable_gaussianCoshAverage_field line 616
  64. def OAI.SKCavity.cavityDoubledCoeff line 620
  65. lemma OAI.SKCavity.integral_gaussianCoshAverage line 623
  66. theorem OAI.SKCavity.averaged_gaussian_sample_error line 650
  67. theorem OAI.SKCavity.averaged_gaussian_cosh_sample_error line 662