OAI/Probability/ParisiFinite/ParisiFiniteTransport.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Parisi Finite Transport.

  1. def OAI.ParisiFinite.smoothEvolve line 23
  2. lemma OAI.ParisiFinite.smoothEvolve_val line 27
  3. def OAI.ParisiFinite.scheduleField line 33
  4. def OAI.ParisiFinite.scheduleDerivative line 39
  5. lemma OAI.ParisiFinite.scheduleField_start line 45
  6. lemma OAI.ParisiFinite.scheduleField_after line 60
  7. lemma OAI.ParisiFinite.scheduleField_PDE line 71
  8. structure OAI.ParisiFinite.GeneralScheduleTimeRealization line 90
  9. def OAI.ParisiFinite.generalScheduleTimeRealization line 99
  10. lemma OAI.ParisiFinite.generalSchedule_verification line 147
  11. lemma OAI.ParisiFinite.finiteTimeCoefficient_nonneg line 182
  12. lemma OAI.ParisiFinite.generalSchedule_terminal_comparison line 190
  13. lemma OAI.ParisiFinite.generalSchedule_actual_transport line 249
  14. def OAI.ParisiSpectral.PositiveDefinite line 307
  15. def OAI.ParisiSpectral.operatorKernel line 313
  16. lemma OAI.ParisiSpectral.operatorKernel_posSemidef line 316
  17. abbrev OAI.ParisiSpectral.KernelHilbert line 342
  18. def OAI.ParisiSpectral.kernelFeature line 344
  19. lemma OAI.ParisiSpectral.inner_kernelFeature line 347
  20. lemma OAI.ParisiSpectral.norm_kernelFeature_sq line 355
  21. lemma OAI.ParisiSpectral.norm_kernelFeature_sub_sq line 359
  22. lemma OAI.ParisiSpectral.continuous_kernelFeature line 364
  23. lemma OAI.ParisiSpectral.posSemidef_inner line 385
  24. lemma OAI.ParisiSpectral.posSemidef_kernel_average line 399
  25. lemma OAI.ParisiSpectral.PositiveDefinite.at_zero line 415
  26. lemma OAI.ParisiSpectral.PositiveDefinite.even line 418
  27. lemma OAI.ParisiSpectral.PositiveDefinite.mul line 421
  28. lemma OAI.ParisiSpectral.PositiveDefinite.add line 424
  29. lemma OAI.ParisiSpectral.PositiveDefinite.smul line 427
  30. lemma OAI.ParisiSpectral.PositiveDefinite.comp_linear line 430
  31. lemma OAI.ParisiSpectral.PositiveDefinite.constant line 436
  32. lemma OAI.ParisiSpectral.PositiveDefinite.pow line 446
  33. lemma OAI.ParisiSpectral.PositiveDefinite.norm_le line 451
  34. lemma OAI.ParisiSpectral.PositiveDefinite.continuous_feature line 462
  35. lemma OAI.ParisiSpectral.PositiveDefinite.posSemidef_limit line 469
  36. lemma OAI.ParisiSpectral.PositiveDefinite.limit line 488
  37. def OAI.ParisiSpectral.heat line 498
  38. lemma OAI.ParisiSpectral.gaussian_double_difference line 501
  39. lemma OAI.ParisiSpectral.PositiveDefinite.heat line 519
  40. lemma OAI.ParisiSpectral.gamma_laplace line 558
  41. lemma OAI.ParisiSpectral.gamma_laplace_integrable line 565
  42. def OAI.ParisiSpectral.hyperbolicFeature line 572
  43. lemma OAI.ParisiSpectral.hyperbolicFeature_mul line 574
  44. lemma OAI.ParisiSpectral.exp_sum_cosh line 581
  45. lemma OAI.ParisiSpectral.hyperbolic_gram_integral line 594
  46. lemma OAI.ParisiSpectral.hyperbolic_gram_integrable line 620
  47. lemma OAI.ParisiSpectral.posSemidef_integral_gram line 632
  48. theorem OAI.ParisiSpectral.cosh_neg_rpow_posSemidef line 671