OAI/Probability/ParisiFinite/SquareKernel.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Square Kernel.

  1. def OAI.ParisiGuerra.squareKernel line 58
  2. lemma OAI.ParisiGuerra.replica_frontier line 60
  3. def OAI.ParisiGuerra.siteCorrection line 76
  4. def OAI.ParisiGuerra.jumpSquares line 83
  5. lemma OAI.ParisiGuerra.jumpSquares_eq line 87
  6. lemma OAI.ParisiGuerra.site_remainder line 95
  7. def OAI.ParisiGuerra.OrderedFrom line 133
  8. lemma OAI.ParisiGuerra.orderedFrom_of_pairwise line 137
  9. lemma OAI.ParisiGuerra.admissible_ordered line 148
  10. lemma OAI.ParisiGuerra.siteCorrection_nonneg line 151
  11. lemma OAI.ParisiGuerra.frontier_add_coordinates line 173
  12. lemma OAI.ParisiGuerra.complete_covariance line 184
  13. lemma OAI.ParisiGuerra.complete_diagonal line 191
  14. def OAI.ParisiGuerra.correction line 201
  15. lemma OAI.ParisiGuerra.correction_nonneg line 205
  16. lemma OAI.ParisiGuerra.complete_remainder line 209
  17. lemma OAI.ParisiGuerra.hasDerivAt_pressureCurve line 228
  18. lemma OAI.ParisiGuerra.continuous_dot_at line 248
  19. lemma OAI.ParisiGuerra.continuous_weighted_correction line 252
  20. lemma OAI.ParisiGuerra.hasDerivAt_correctedCurve line 272
  21. lemma OAI.ParisiGuerra.curve_sum_rule line 282
  22. lemma OAI.ParisiGuerra.integrated_correction_nonneg line 294
  23. lemma OAI.ParisiGuerra.curve_upper_bound line 305
  24. lemma OAI.ParisiFinite.hierarchyValue_append line 318
  25. def OAI.ParisiGuerra.siteField line 327
  26. lemma OAI.ParisiGuerra.siteField_zero line 329
  27. lemma OAI.ParisiGuerra.siteField_update line 331
  28. lemma OAI.ParisiGuerra.site_sum_update line 346
  29. lemma OAI.ParisiGuerra.ambientStep_site line 355
  30. lemma OAI.ParisiGuerra.siteList_endpoint line 367
  31. lemma OAI.ParisiGuerra.siteBlock_endpoint line 391
  32. lemma OAI.ParisiGuerra.spinTrace_site line 405
  33. lemma OAI.ParisiGuerra.siteCoordinates_endpoint line 413
  34. lemma OAI.ParisiGuerra.costBlock_zero line 423
  35. lemma OAI.ParisiGuerra.pressureCurve_zero line 434
  36. lemma OAI.ParisiFinite.integrable_gaussian_linear line 449
  37. lemma OAI.ParisiFinite.integral_gaussian_fin_cons line 470
  38. lemma OAI.ParisiFinite.hierarchyValue_gaussian line 486
  39. lemma OAI.ParisiGuerra.siteCoordinates_zero_width line 517
  40. lemma OAI.ParisiGuerra.costBlock_expectation line 528
  41. lemma OAI.ParisiGuerra.pressureCurve_pi_div_two line 547
  42. lemma OAI.ParisiGuerra.freeEnergy_sum_rule line 554
  43. lemma OAI.ParisiGuerra.freeEnergy_le_functional line 567
  44. lemma OAI.ParisiGuerra.limitingFreeEnergy_le_functional line 572
  45. def OAI.SKCavity.kernel line 587
  46. lemma OAI.SKCavity.squared_increment line 590
  47. lemma OAI.SKCavity.kernel_scale line 597
  48. lemma OAI.SKCavity.expected_logPartition_eq_of_kernel line 606
  49. def OAI.SKCavity.coreScale line 617
  50. def OAI.SKCavity.cavityScale line 619
  51. lemma OAI.SKCavity.coreScale_sq line 621
  52. lemma OAI.SKCavity.cavityScale_sq line 625
  53. lemma OAI.SKCavity.scales_sum line 629
  54. def OAI.SKCavity.cavityCoeff line 634
  55. lemma OAI.SKCavity.overlapSum_last line 638
  56. lemma OAI.SKCavity.cavityCoeff_kernel line 644
  57. def OAI.SKCavity.correctedCoeff line 674
  58. lemma OAI.SKCavity.correctedCoeff_kernel line 677
  59. lemma OAI.SKCavity.expected_cavity_pressure line 685
  60. lemma OAI.SKCavity.expected_corrected_pressure line 694