OAI/Probability/ParisiFinite/MixedReplicaIdentity.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Mixed Replica Identity.

  1. theorem OAI.SKCavity.mixed_replica_identity line 63
  2. lemma OAI.SKCavity.mixed_energyMean line 93
  3. def OAI.SKCavity.mixedGGDefect line 110
  4. theorem OAI.SKCavity.mixedGGDefect_identity line 123
  5. theorem OAI.SKCavity.mixedGGDefect_bound line 148
  6. lemma OAI.SKCavity.mixed_energyMean_bounds line 157
  7. lemma OAI.SKCavity.continuous_field_coeff line 181
  8. lemma OAI.SKCavity.continuous_gibbsMean_first line 185
  9. lemma OAI.SKCavity.continuous_gibbsCov_first line 190
  10. lemma OAI.SKCavity.continuous_energyMean_coeff line 194
  11. lemma OAI.SKCavity.abs_energyMean_le line 206
  12. def OAI.SKCavity.energyVariance line 214
  13. lemma OAI.SKCavity.energyVariance_nonneg line 217
  14. lemma OAI.SKCavity.continuous_energyVariance_coeff line 220
  15. lemma OAI.SKCavity.abs_energyVariance_le line 230
  16. lemma OAI.SKCavity.varianceLine_eq_energyVariance line 238
  17. def OAI.SKCavity.intervalLaw line 250
  18. instance OAI.SKCavity.intervalLaw_isFiniteMeasure line 252
  19. lemma OAI.SKCavity.intervalLaw_probability line 256
  20. lemma OAI.SKCavity.intervalLaw_ae line 263
  21. lemma OAI.SKCavity.integral_intervalLaw line 266
  22. abbrev OAI.SKCavity.boxLaw line 272
  23. lemma OAI.SKCavity.boxLaw_ae line 274
  24. lemma OAI.SKCavity.integral_boxLaw_coordinate line 280
  25. theorem OAI.SKCavity.exists_box_sum_le line 295
  26. lemma OAI.SKCavity.continuous_mixedCoeff line 344
  27. lemma OAI.SKCavity.continuous_shiftCoord line 355
  28. def OAI.SKCavity.mixedError line 366
  29. lemma OAI.SKCavity.continuous_mixedError line 371
  30. lemma OAI.SKCavity.mixedError_bounded line 381
  31. lemma OAI.SKCavity.mixedError_as_line line 402
  32. lemma OAI.SKCavity.mixedError_dominates line 410
  33. lemma OAI.SKCavity.mixedError_insert line 448
  34. lemma OAI.SKCavity.integral_mixedError_le line 456
  35. theorem OAI.SKCavity.exists_mixed_energy_amplitude line 490
  36. theorem OAI.SKCavity.exists_mixed_GG_amplitude line 511
  37. lemma OAI.SKCavity.increment_mixed_sub line 534
  38. lemma OAI.SKCavity.abs_increment_mixed_sub_le line 554
  39. theorem OAI.SKCavity.mixed_pressure_error line 575
  40. lemma OAI.SKCavity.mixed_root_pressure_bound line 590
  41. lemma OAI.SKCavity.mixed_root_GG_bound line 613
  42. lemma OAI.SKCavity.exists_mixed_root_amplitude line 634
  43. def OAI.SKCavity.allPowerRoot line 653
  44. def OAI.SKCavity.powerCutoff line 654
  45. lemma OAI.SKCavity.allPowerRoot_nonneg line 656
  46. lemma OAI.SKCavity.allPowerRoot_pow_four line 657
  47. lemma OAI.SKCavity.one_le_allPowerRoot line 664
  48. lemma OAI.SKCavity.tendsto_allPowerRoot line 667
  49. lemma OAI.SKCavity.tendsto_powerCutoff line 669
  50. lemma OAI.SKCavity.powerCutoff_cast_bound line 672
  51. lemma OAI.SKCavity.allPower_GG_rate line 679
  52. lemma OAI.SKCavity.allPower_amplitude_variance_density line 698