OAI/Probability/ParisiFinite/ScheduleWidthNonneg.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Schedule Width Nonneg.

  1. lemma OAI.ParisiFinite.schedule_width_nonneg line 64
  2. lemma OAI.ParisiFinite.evolution_lyapunov line 71
  3. lemma OAI.ParisiFinite.integrable_smooth_d2 line 121
  4. lemma OAI.ParisiFinite.evolution_terminal_curvature_le line 127
  5. lemma OAI.ParisiFinite.terminal_curvature_minorant line 157
  6. lemma OAI.ParisiFinite.finite_curvature_lower line 178
  7. def OAI.ParisiFinite.curvatureFloor line 210
  8. lemma OAI.ParisiFinite.curvatureFloor_pos line 213
  9. lemma OAI.ParisiFinite.finite_curvature_floor line 217
  10. lemma OAI.ParisiFinite.finite_gradient_floor line 232
  11. lemma OAI.ParisiFinite.fieldGradient_dyadic_tendsto line 256
  12. lemma OAI.ParisiFinite.fieldGradient_floor line 267
  13. lemma OAI.ParisiFinite.fieldGradient_strictMono line 277
  14. lemma OAI.ParisiFinite.integrable_smooth_d1_sq line 295
  15. lemma OAI.ParisiFinite.smooth_integral_sq_sub line 300
  16. lemma OAI.ParisiFinite.integrable_smooth_d1_sq_sub line 310
  17. lemma OAI.ParisiFinite.transition_gradient_variance line 317
  18. lemma OAI.ParisiFinite.transition_gradient_variance_le line 325
  19. lemma OAI.ParisiFinite.transition_d1_sq_le_time line 352
  20. lemma OAI.ParisiFinite.evolution_d1_sq_le_time line 369
  21. lemma OAI.ParisiFinite.evolution_gradient_variance_le line 399
  22. lemma OAI.ParisiFinite.terminal_gradient_scaled_deriv line 415
  23. lemma OAI.ParisiFinite.terminal_gradient_ratio_tendsto line 420
  24. lemma OAI.ParisiFinite.terminal_gradient_ratio_bound line 426
  25. lemma OAI.ParisiFinite.terminal_magnetization_ratio_second_moment line 437
  26. def OAI.ParisiFinite.replicaTrial line 467
  27. lemma OAI.ParisiFinite.terminal_curvature_identity line 470
  28. lemma OAI.ParisiFinite.replicaTrial_hasDerivAt line 480
  29. lemma OAI.ParisiFinite.replicaTrial_zero line 499
  30. lemma OAI.ParisiFinite.exists_replicaTrial_decrease line 502
  31. lemma OAI.ParisiFinite.pressure_lt_annealed line 538
  32. lemma OAI.ParisiFinite.dyadicEvolution_constant line 556
  33. def OAI.ParisiFinite.zeroOrderMeasure line 570
  34. lemma OAI.ParisiFinite.zeroOrderMeasure_coefficient line 573
  35. lemma OAI.ParisiFinite.zeroOrderMeasure_functional line 579
  36. lemma OAI.ParisiFinite.zeroOrderMeasure_not_minimizing line 595
  37. lemma OAI.ParisiFinite.shift_integrableExpSet line 612
  38. lemma OAI.ParisiFinite.expMass_hasDerivAt_coefficient line 618
  39. lemma OAI.ParisiFinite.step_hasDerivAt_coefficient line 630
  40. lemma OAI.ParisiFinite.coefficient_cgf_second_variance line 646
  41. lemma OAI.ParisiFinite.analytic_dslope_hasDerivAt line 668
  42. lemma OAI.ParisiFinite.step_eq_cgf_dslope line 683
  43. lemma OAI.ParisiFinite.step_hasDerivAt_zero_coefficient line 698
  44. lemma OAI.ParisiFinite.step_analyticAt_coefficient line 714