OAI/Probability/ParisiFinite/ParisiConjugateTransport.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Parisi Conjugate Transport.

  1. lemma OAI.ParisiSpectral.CoshCone.neg_exp_positiveDefinite line 22
  2. lemma OAI.ParisiSpectral.evolve_coshCone line 34
  3. lemma OAI.ParisiSpectral.evolve_neg_exp_positiveDefinite line 49
  4. lemma OAI.ParisiSpectral.linearEvolve_continuous_bound line 59
  5. lemma OAI.ParisiSpectral.heat_eq_standard line 68
  6. lemma OAI.ParisiSpectral.exp_step_all line 80
  7. lemma OAI.ParisiSpectral.conjugate_tiltedMean line 86
  8. lemma OAI.ParisiSpectral.conjugate_linearEvolve_positiveDefinite line 104
  9. lemma OAI.ParisiFinite.compact_convolution_bound line 151
  10. def OAI.ParisiFinite.boundedMollify line 166
  11. lemma OAI.ParisiFinite.boundedMollify_bound line 185
  12. lemma OAI.ParisiFinite.tiltedMean_tendsto_terminal line 189
  13. lemma OAI.ParisiFinite.linearEvolve_tendsto_terminal line 205
  14. lemma OAI.ParisiFinite.generalSchedule_actual_transport_continuous line 219
  15. lemma OAI.ParisiPath.brownian_solution_time_generator_between line 259
  16. lemma OAI.ParisiFinite.generalSchedule_terminal_comparison_between line 290
  17. lemma OAI.ParisiFinite.hasDerivAt_expected_evolve_terminal line 342
  18. lemma OAI.ParisiFinite.generalSchedule_actual_transport_between line 371
  19. lemma OAI.ParisiFinite.generalSchedule_actual_transport_between_continuous line 414
  20. lemma OAI.ParisiPath.drift_comp_tendsto_at line 466
  21. lemma OAI.ParisiPath.next_tendsto_drift_ae line 482
  22. lemma OAI.ParisiPath.iterate_tendsto_drift_ae line 516
  23. theorem OAI.ParisiPath.solution_tendsto_drift_ae line 526