OAI/Probability/ParisiFinite/Mix.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Mix.

  1. def OAI.ParisiFinite.BoundedCoefficient.mix line 19
  2. lemma OAI.ParisiFinite.BoundedCoefficient.mix_real line 26
  3. lemma OAI.ParisiFinite.BoundedCoefficient.mix_difference line 30
  4. lemma OAI.ParisiFinite.BoundedCoefficient.mix_tendsto line 33
  5. lemma OAI.ParisiFinite.BoundedCoefficient.norm_direction_le line 42
  6. def OAI.ParisiFinite.BoundedCoefficient.variationIntegral line 51
  7. lemma OAI.ParisiFinite.BoundedCoefficient.variation_integrable line 55
  8. lemma OAI.ParisiFinite.BoundedCoefficient.variationIntegral_tendsto line 61
  9. theorem OAI.ParisiFinite.BoundedCoefficient.field_first_variation line 82
  10. lemma OAI.ParisiFinite.BoundedCoefficient.penalty_mix_sub line 120
  11. def OAI.ParisiFinite.BoundedCoefficient.firstVariation line 135
  12. lemma OAI.ParisiFinite.BoundedCoefficient.firstVariation_eq line 139
  13. theorem OAI.ParisiFinite.BoundedCoefficient.functional_first_variation line 155
  14. def OAI.ParisiFinite.probabilityMix line 183
  15. lemma OAI.ParisiFinite.probabilityMix_real line 191
  16. lemma OAI.ParisiFinite.probabilityMix_coefficient_real line 200
  17. lemma OAI.ParisiFinite.probabilityMix_coefficient line 222
  18. theorem OAI.ParisiFinite.measureFunctional_first_variation line 235
  19. theorem OAI.ParisiFinite.minimizingParisi_firstVariation_nonneg line 249
  20. lemma OAI.ParisiFinite.integral_cdf_mul line 278
  21. lemma OAI.ParisiFinite.measureCDF_mono line 319
  22. lemma OAI.ParisiFinite.ofMeasure_real line 324
  23. def OAI.ParisiFinite.deviation line 332
  24. def OAI.ParisiFinite.variationalPotential line 336
  25. lemma OAI.ParisiFinite.continuous_deviation line 340
  26. lemma OAI.ParisiFinite.norm_deviation_le line 343
  27. lemma OAI.ParisiFinite.hasDerivAt_variationalPotential line 349
  28. lemma OAI.ParisiFinite.continuous_variationalPotential line 356
  29. lemma OAI.ParisiFinite.variationalPotential_integrable line 360
  30. lemma OAI.ParisiFinite.firstVariation_potential line 367
  31. lemma OAI.ParisiFinite.minimizingParisi_potential_average_le line 390
  32. lemma OAI.ParisiFinite.minimizingParisi_potential_average_le_point line 400
  33. theorem OAI.ParisiFinite.minimizingParisi_support_potential line 410
  34. lemma OAI.ParisiFinite.expectedProduct_zero line 450
  35. lemma OAI.ParisiFinite.expectedProduct_one_lt line 460
  36. lemma OAI.ParisiFinite.minimizingParisi_deviation_interior line 483
  37. lemma OAI.ParisiFinite.minimizingParisi_one_not_mem_support line 493
  38. theorem OAI.ParisiFinite.minimizingParisi_selfConsistency line 515
  39. def OAI.ParisiFinite.BoundedCoefficient.curvature line 543
  40. lemma OAI.ParisiFinite.BoundedCoefficient.curvature_eq line 546
  41. lemma OAI.ParisiFinite.BoundedCoefficient.continuous_curvature line 550
  42. lemma OAI.ParisiFinite.BoundedCoefficient.norm_curvature_le line 557
  43. lemma OAI.ParisiFinite.BoundedCoefficient.curvature_pos line 560
  44. lemma OAI.ParisiFinite.BoundedCoefficient.curvature_aestronglyMeasurable line 566
  45. lemma OAI.ParisiFinite.BoundedCoefficient.curvature_square_integrable line 573
  46. def OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature line 582
  47. lemma OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature_continuous line 586
  48. lemma OAI.ParisiFinite.BoundedCoefficient.spin_mean_square_evolution line 596
  49. lemma OAI.ParisiFinite.BoundedCoefficient.hasDerivAt_expectedProduct_self line 626