OAI/Probability/ParisiFinite/CanonicalSpatialTest.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Canonical Spatial Test.

  1. def OAI.ParisiFinite.canonicalSpatialTest line 19
  2. lemma OAI.ParisiFinite.finite_schedule_verification_at line 32
  3. lemma OAI.ParisiFinite.expected_global_dyadic_field_tendsto line 70
  4. theorem OAI.ParisiFinite.canonical_verification_at line 94
  5. lemma OAI.ParisiFinite.minimizingParisi_potential_average_eq line 154
  6. lemma OAI.ParisiFinite.ofMeasure_real_after_support line 167
  7. lemma OAI.ParisiFinite.minimizingParisi_weighted_deviation line 175
  8. lemma OAI.ParisiFinite.minimizingParisi_weighted_consistency line 211
  9. lemma OAI.ParisiFinite.BoundedCoefficient.curvature_integrable line 248
  10. def OAI.ParisiFinite.BoundedCoefficient.expectedCurvature line 255
  11. lemma OAI.ParisiFinite.BoundedCoefficient.expectedCurvature_continuous line 259
  12. lemma OAI.ParisiFinite.BoundedCoefficient.expectedCurvature_nonneg line 267
  13. lemma OAI.ParisiFinite.BoundedCoefficient.expectedCurvature_bound line 270
  14. lemma OAI.ParisiFinite.BoundedCoefficient.position_spin line 275
  15. lemma OAI.ParisiFinite.BoundedCoefficient.field_value_at line 316
  16. lemma OAI.ParisiFinite.minimizingParisi_position_spin line 345
  17. lemma OAI.ParisiFinite.minimizingParisi_field_value_at line 356
  18. lemma OAI.ParisiFinite.terminal_entropy_loss line 379
  19. lemma OAI.ParisiFinite.measureFunctional_eq_field_penalty line 419
  20. lemma OAI.ParisiFinite.minimizingParisi_value_eq_pressure line 426
  21. lemma OAI.ParisiFinite.measureCoefficient_penalty_split line 431
  22. lemma OAI.ParisiFinite.minimizingParisi_value_at_endpoint_raw line 451
  23. theorem OAI.ParisiFinite.minimizingParisi_value_at_endpoint line 502
  24. theorem OAI.ParisiFinite.minimizingParisi_zero_in_support line 535
  25. theorem OAI.ParisiFinite.minimizingParisi_support_boundary line 542
  26. theorem OAI.ParisiFinite.exists_minimizingParisi_endpoint_value line 555
  27. abbrev OAI.ParisiGapGeometry.OrderPoint line 585
  28. theorem OAI.ParisiGapGeometry.support_gap_endpoints line 587
  29. theorem OAI.ParisiGapGeometry.cdf_constant_on_gap line 608
  30. theorem OAI.ParisiGapGeometry.cdf_pos_at_gap_left line 622