OAI/Probability/ParisiFinite/ParisiCanonicalTransport.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Parisi Canonical Transport.

  1. lemma OAI.ParisiFinite.smoothEvolve_curvature line 21
  2. lemma OAI.ParisiFinite.scheduleField_curvature line 30
  3. abbrev OAI.ParisiFinite.genericRecursion line 43
  4. lemma OAI.ParisiFinite.scheduleField_suffix_val line 45
  5. lemma OAI.ParisiFinite.evolve_suffix_time_bound line 67
  6. lemma OAI.ParisiFinite.general_shifted_schedule_suffix_error line 99
  7. lemma OAI.ParisiFinite.general_dyadic_suffix_grid_error line 151
  8. lemma OAI.ParisiFinite.general_dyadic_suffix_value_error line 170
  9. lemma OAI.ParisiFinite.general_dyadic_field_tendstoUniformly line 185
  10. lemma OAI.ParisiFinite.general_dyadic_gradient_tendstoUniformly line 200
  11. lemma OAI.ParisiFinite.canonicalSmoothField_curvature line 211
  12. lemma OAI.ParisiFinite.prefix_dyadic_gradient_tendstoUniformly line 218
  13. lemma OAI.ParisiFinite.scheduleField_measurable_d1 line 241
  14. lemma OAI.ParisiFinite.finiteTimeCoefficient_continuous_ae line 256
  15. def OAI.ParisiFinite.scheduleDrift line 271
  16. lemma OAI.ParisiFinite.scheduleDrift_joint_ae_continuous line 296
  17. def OAI.ParisiPath.patchDrift line 312
  18. lemma OAI.ParisiPath.continuousAt_patch_Ioo line 318
  19. lemma OAI.ParisiPath.patchDrift_joint_ae_continuous line 337
  20. lemma OAI.ParisiFinite.prefix_dyadic_coefficient_tendsto_ae line 347
  21. def OAI.ParisiFinite.BoundedCoefficient.prefixDrift line 369
  22. lemma OAI.ParisiFinite.BoundedCoefficient.prefixDrift_joint_ae_continuous line 374
  23. lemma OAI.ParisiFinite.BoundedCoefficient.prefixDrift_tendsto_ae line 381
  24. lemma OAI.ParisiFinite.BoundedCoefficient.prefix_solution_tendsto line 395
  25. lemma OAI.ParisiFinite.BoundedCoefficient.actual_conjugate_positive_continuous line 409
  26. lemma OAI.ParisiFinite.BoundedCoefficient.conjugate_expectation_nonneg line 461
  27. def OAI.ParisiSpectral.stepWeight line 494
  28. def OAI.ParisiSpectral.stepJoint line 497
  29. def OAI.ParisiSpectral.stepLaw line 500
  30. lemma OAI.ParisiSpectral.stepWeight_pos line 503
  31. lemma OAI.ParisiSpectral.continuous_stepWeight line 506
  32. lemma OAI.ParisiSpectral.integral_stepWeight line 514
  33. lemma OAI.ParisiSpectral.stepJoint_probability line 520
  34. lemma OAI.ParisiSpectral.integral_stepJoint line 533
  35. lemma OAI.ParisiSpectral.integral_stepLaw line 549
  36. lemma OAI.ParisiSpectral.measure_eq_stepLaw line 556
  37. lemma OAI.ParisiFinite.BoundedCoefficient.actual_plateau_transport line 582
  38. lemma OAI.ParisiFinite.BoundedCoefficient.actual_plateau_law line 607
  39. lemma OAI.ParisiFinite.BoundedCoefficient.actual_plateau_transport_integrable line 630