OAI/Probability/ParisiFinite/ThermalDeviation.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Thermal Deviation.

  1. def OAI.SKCavity.thermalDeviation line 61
  2. lemma OAI.SKCavity.thermalDeviation_nonneg line 64
  3. lemma OAI.SKCavity.thermalDeviation_le line 67
  4. lemma OAI.SKCavity.gibbsCov_eq_centered line 80
  5. lemma OAI.SKCavity.thermalDeviation_sq_le line 92
  6. lemma OAI.SKCavity.continuous_thermalDeviation_field line 103
  7. lemma OAI.SKCavity.memLp_thermalDeviation_field line 117
  8. lemma OAI.SKCavity.expected_thermalDeviation_le line 125
  9. theorem OAI.SKCavity.energyDeviation_le_thermal_add line 143
  10. def OAI.SKCavity.pressureFluctuation line 176
  11. def OAI.SKCavity.disorderDeviation line 179
  12. lemma OAI.SKCavity.integrable_pressureFluctuation line 182
  13. lemma OAI.SKCavity.pressureFluctuation_le line 186
  14. lemma OAI.SKCavity.disorderDeviation_nonneg line 191
  15. theorem OAI.SKCavity.disorderDeviation_le line 196
  16. lemma OAI.SKCavity.continuous_meanLine line 249
  17. lemma OAI.SKCavity.continuous_varianceLine line 252
  18. lemma OAI.SKCavity.integral_meanLine line 262
  19. lemma OAI.SKCavity.integral_varianceLine line 267
  20. lemma OAI.SKCavity.integral_meanLine_increment_le line 274
  21. lemma OAI.SKCavity.meanLine_eq_energyMean line 305
  22. lemma OAI.SKCavity.energyDeviation_amplitude_bound line 309
  23. theorem OAI.SKCavity.exists_amplitude_energyDeviation line 331
  24. lemma OAI.SKCavity.affineCoeff_perturbed line 373
  25. lemma OAI.SKCavity.pSpin_meanLine line 378
  26. lemma OAI.SKCavity.pSpin_energyMean_bounds line 383
  27. lemma OAI.SKCavity.pSpin_pressureFluctuation_le line 398
  28. theorem OAI.SKCavity.exists_pSpin_energy_amplitude line 405
  29. theorem OAI.SKCavity.exists_pSpin_GG_amplitude line 443
  30. def OAI.SKCavity.eighthRootScale line 465
  31. lemma OAI.SKCavity.eighthRootScale_nonneg line 467
  32. lemma OAI.SKCavity.eighthRootScale_pow_eight line 469
  33. lemma OAI.SKCavity.one_le_eighthRootScale line 479
  34. lemma OAI.SKCavity.tendsto_eighthRootScale line 486
  35. lemma OAI.SKCavity.eighthRoot_pressure_scale_bound line 490
  36. lemma OAI.SKCavity.eighthRoot_GG_bound line 510
  37. lemma OAI.SKCavity.eighthRoot_amplitude_pressure_bound line 529
  38. lemma OAI.SKCavity.exists_rootScale_GG_amplitude line 550
  39. def OAI.SKCavity.genericPSpinAmplitude line 562
  40. lemma OAI.SKCavity.genericPSpinAmplitude_mem line 565
  41. lemma OAI.SKCavity.genericPSpinAmplitude_defect_le line 570
  42. theorem OAI.SKCavity.tendsto_genericPSpin_GG_defect line 578
  43. lemma OAI.SKCavity.tendsto_genericPSpin_amplitude_squared_density line 591
  44. theorem OAI.SKCavity.tendsto_genericPSpin_pressureDensity_error line 603
  45. abbrev OAI.SKCavity.MixedIndex line 616
  46. def OAI.SKCavity.mixedCoeff line 620
  47. def OAI.SKCavity.mixedNoise line 625
  48. lemma OAI.SKCavity.mixedCoeff_kernel line 629
  49. lemma OAI.SKCavity.mixedNoise_crossCov line 641
  50. lemma OAI.SKCavity.mixedCoeff_abs line 662
  51. lemma OAI.SKCavity.mixedCoeff_diag line 670
  52. lemma OAI.SKCavity.mixed_pressureFluctuation_le line 681
  53. lemma OAI.SKCavity.affineCoeff_mixed_update line 690