OAI/Probability/ParisiFinite/IncrementEqKernel.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Increment Eq Kernel.

  1. lemma OAI.SKCavity.increment_eq_kernel line 60
  2. lemma OAI.SKCavity.increment_perturbed_sub line 68
  3. lemma OAI.SKCavity.abs_increment_perturbed_sub_le line 81
  4. theorem OAI.SKCavity.perturbed_pressure_error line 97
  5. theorem OAI.SKCavity.tendsto_perturbed_pressureDensity_error line 107
  6. def OAI.SKCavity.perturbationNoise line 131
  7. lemma OAI.SKCavity.perturbationNoise_crossCov line 134
  8. theorem OAI.SKCavity.pSpin_replica_identity line 147
  9. lemma OAI.ParisiFinite.gibbsCov_self_nonneg line 185
  10. lemma OAI.ParisiFinite.monotone_gibbsMean_line line 204
  11. lemma OAI.ParisiFinite.hasDerivAt_logPartition_line line 211
  12. lemma OAI.ParisiFinite.convex_logPartition_line line 215
  13. theorem OAI.ParisiFinite.convex_derivative_deviation line 226
  14. lemma OAI.SKCavity.norm_field_le_sum line 271
  15. lemma OAI.SKCavity.integrable_norm_field line 279
  16. lemma OAI.SKCavity.memLp_field_two line 287
  17. lemma OAI.SKCavity.memLp_norm_field_two line 298
  18. lemma OAI.SKCavity.integrable_norm_field_sq line 307
  19. def OAI.SKCavity.affineCoeff line 319
  20. lemma OAI.SKCavity.field_affineCoeff line 322
  21. def OAI.SKCavity.expectedLine line 332
  22. def OAI.SKCavity.meanLine line 335
  23. def OAI.SKCavity.varianceLine line 338
  24. lemma OAI.SKCavity.expectedLine_eq line 342
  25. lemma OAI.SKCavity.continuous_lineMean line 346
  26. lemma OAI.SKCavity.continuous_lineVariance line 359
  27. lemma OAI.SKCavity.integrable_lineMean line 376
  28. lemma OAI.SKCavity.integrable_lineVariance line 382
  29. theorem OAI.SKCavity.hasDerivAt_expectedLine line 392
  30. theorem OAI.SKCavity.hasDerivAt_meanLine line 407
  31. lemma OAI.SKCavity.varianceLine_nonneg line 422
  32. lemma OAI.SKCavity.monotone_meanLine line 425
  33. lemma OAI.SKCavity.convex_expectedLine line 430
  34. def OAI.SKCavity.averagedReplica line 445
  35. lemma OAI.SKCavity.replicaMean_const line 448
  36. lemma OAI.SKCavity.replicaMean_add line 453
  37. lemma OAI.SKCavity.replicaMean_sub line 458
  38. lemma OAI.SKCavity.replicaMean_const_mul line 463
  39. lemma OAI.SKCavity.averagedReplica_const line 467
  40. lemma OAI.SKCavity.averagedReplica_add line 471
  41. lemma OAI.SKCavity.averagedReplica_sub line 476
  42. lemma OAI.SKCavity.averagedReplica_const_mul line 482
  43. lemma OAI.SKCavity.averagedReplica_marginal line 486
  44. lemma OAI.SKCavity.averagedReplica_sum line 490
  45. lemma OAI.SKCavity.replicaMean_abs_bound line 500
  46. lemma OAI.SKCavity.averagedReplica_abs_bound line 511
  47. def OAI.SKCavity.energyMean line 519
  48. def OAI.SKCavity.energyObservation line 522
  49. lemma OAI.SKCavity.energyObservation_one line 525
  50. def OAI.SKCavity.energyDeviation line 541
  51. lemma OAI.SKCavity.integrable_energyDeviation line 544
  52. lemma OAI.SKCavity.energyDeviation_nonneg line 554
  53. lemma OAI.SKCavity.energyObservation_sub_mean line 559
  54. theorem OAI.SKCavity.energyObservation_covariance_bound line 579
  55. lemma OAI.GaussianConcentration.integral_abs_centered_le_sqrt_variance line 622
  56. lemma OAI.GaussianConcentration.memLp_logPartition_field line 636
  57. lemma OAI.GaussianConcentration.logPartition_absolute_fluctuation line 653
  58. lemma OAI.SKCavity.pSpin_energyMean line 667
  59. def OAI.SKCavity.pSpinGGDefect line 684
  60. theorem OAI.SKCavity.pSpinGGDefect_identity line 697
  61. theorem OAI.SKCavity.pSpinGGDefect_bound line 722