OAI/Probability/ParisiFinite/SpinTrace.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Spin Trace.

  1. def OAI.ParisiFinite.spinTrace line 59
  2. def OAI.ParisiFinite.gibbsMean line 61
  3. def OAI.ParisiFinite.gibbsCov line 63
  4. lemma OAI.ParisiFinite.continuous_gibbsMean line 66
  5. lemma OAI.ParisiFinite.continuous_gibbsCov line 72
  6. lemma OAI.ParisiFinite.abs_gibbsMean_le line 75
  7. lemma OAI.ParisiFinite.abs_gibbsCov_le line 78
  8. lemma OAI.ParisiFinite.hasDerivAt_spinTrace line 91
  9. lemma OAI.ParisiFinite.hasDerivAt_gibbsMean line 105
  10. lemma OAI.ParisiFinite.spinTrace_lipschitz line 124
  11. def OAI.ParisiFinite.traceField line 138
  12. lemma OAI.ParisiFinite.ambient_exp_bound line 165
  13. lemma OAI.ParisiFinite.continuous_parameterMoment line 182
  14. lemma OAI.ParisiFinite.continuous_parameterMass line 219
  15. lemma OAI.ParisiFinite.continuous_parameterTilt line 227
  16. lemma OAI.ParisiFinite.continuous_parameterAverage line 238
  17. lemma OAI.ParisiFinite.continuous_parameterStep line 269
  18. lemma OAI.ParisiFinite.hasDerivAt_parameterMass line 292
  19. lemma OAI.ParisiFinite.hasDerivAt_parameterAverage line 333
  20. lemma OAI.ParisiFinite.hasDerivAt_parameterStep line 358
  21. lemma OAI.ParisiFinite.hasDerivAt_bivariate_path line 389
  22. structure OAI.ParisiFinite.FieldFamily line 419
  23. lemma OAI.ParisiFinite.FieldFamily.square_bound line 441
  24. def OAI.ParisiFinite.FieldFamily.constant line 446
  25. lemma OAI.ParisiFinite.FieldFamily.continuous_mapTilt line 464
  26. lemma OAI.ParisiFinite.FieldFamily.continuous_mapStep line 475
  27. def OAI.ParisiFinite.FieldFamily.transformedDot line 484
  28. lemma OAI.ParisiFinite.FieldFamily.hasDerivAt_transformed line 489
  29. lemma OAI.ParisiFinite.FieldFamily.continuous_transformedDot line 525
  30. lemma OAI.ParisiFinite.FieldFamily.bound_transformedDot line 538
  31. def OAI.ParisiFinite.FieldFamily.transform line 558
  32. structure OAI.ParisiFinite.MovingCoordinate line 629
  33. def OAI.ParisiFinite.MovingCoordinate.sine line 641
  34. def OAI.ParisiFinite.MovingCoordinate.cosine line 650
  35. def OAI.ParisiFinite.MovingCoordinate.constant line 659
  36. def OAI.ParisiFinite.hierarchy line 673
  37. def OAI.ParisiFinite.hierarchyValue line 678
  38. lemma OAI.ParisiFinite.hierarchy_val line 682
  39. lemma OAI.ParisiFinite.hasDerivAt_hierarchyValue line 693
  40. lemma OAI.ParisiFinite.hierarchy_dot_cons line 698
  41. lemma OAI.ParisiFinite.ambientStep_zero_direction line 708
  42. lemma OAI.ParisiFinite.hierarchyValue_zero_scales line 713