OAI/Probability/ParisiFinite/MeasurableStepParam.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Measurable Step Param.

  1. lemma OAI.ParisiFinite.measurable_step_param line 16
  2. lemma OAI.ParisiFinite.measurable_evolve_ofFn line 30
  3. lemma OAI.ParisiFinite.measurable_field line 48
  4. lemma OAI.ParisiFinite.measurable_fieldGradient line 67
  5. def OAI.ParisiFinite.parisiDrift line 87
  6. lemma OAI.ParisiFinite.parisiDrift_measurable line 91
  7. lemma OAI.ParisiFinite.parisiDrift_bound line 101
  8. lemma OAI.ParisiFinite.parisiDrift_lipschitz line 113
  9. structure OAI.ParisiFinite.BoundedCoefficient line 148
  10. def OAI.ParisiFinite.BoundedCoefficient.ofMeasure line 156
  11. def OAI.ParisiFinite.BoundedCoefficient.real line 161
  12. lemma OAI.ParisiFinite.BoundedCoefficient.measurable_real line 163
  13. lemma OAI.ParisiFinite.BoundedCoefficient.real_nonneg line 166
  14. lemma OAI.ParisiFinite.BoundedCoefficient.real_le line 167
  15. def OAI.ParisiFinite.BoundedCoefficient.drift line 169
  16. lemma OAI.ParisiFinite.BoundedCoefficient.drift_measurable line 172
  17. lemma OAI.ParisiFinite.BoundedCoefficient.drift_bound line 177
  18. lemma OAI.ParisiFinite.BoundedCoefficient.drift_lipschitz line 182
  19. def OAI.ParisiFinite.BoundedCoefficient.driftData line 191
  20. lemma OAI.ParisiFinite.BoundedCoefficient.drift_joint_ae_continuous line 197
  21. def OAI.ParisiFinite.BoundedCoefficient.spin line 221
  22. lemma OAI.ParisiFinite.BoundedCoefficient.spin_eq line 224
  23. lemma OAI.ParisiFinite.BoundedCoefficient.continuous_spin line 228
  24. lemma OAI.ParisiFinite.BoundedCoefficient.norm_spin_le line 232
  25. lemma OAI.ParisiFinite.BoundedCoefficient.spin_aestronglyMeasurable line 238
  26. lemma OAI.ParisiFinite.BoundedCoefficient.spin_integrable line 245
  27. def OAI.ParisiFinite.BoundedCoefficient.expectedProduct line 252
  28. lemma OAI.ParisiFinite.BoundedCoefficient.norm_spin_product_le line 256
  29. lemma OAI.ParisiFinite.BoundedCoefficient.spin_product_integrable line 261
  30. lemma OAI.ParisiFinite.BoundedCoefficient.expectedProduct_continuous line 269
  31. lemma OAI.ParisiFinite.BoundedCoefficient.expectedProduct_bound line 277
  32. lemma OAI.ParisiFinite.BoundedCoefficient.expectedProduct_comm line 282
  33. lemma OAI.ParisiFinite.BoundedCoefficient.real_intervalIntegrable line 286
  34. lemma OAI.ParisiFinite.BoundedCoefficient.expectedProduct_psd line 291
  35. lemma OAI.ParisiFinite.BoundedCoefficient.weightedProduct_intervalIntegrable line 303
  36. def OAI.ParisiFinite.BoundedCoefficient.feedbackKernel line 308
  37. lemma OAI.ParisiFinite.BoundedCoefficient.feedbackKernel_intervalIntegrable line 313
  38. lemma OAI.ParisiFinite.BoundedCoefficient.expected_verificationKernel_eq_feedback line 321
  39. theorem OAI.ParisiFinite.BoundedCoefficient.feedback_verification line 335
  40. theorem OAI.ParisiFinite.BoundedCoefficient.field_comparison_lower line 345
  41. theorem OAI.ParisiFinite.BoundedCoefficient.field_comparison_upper line 371
  42. lemma OAI.ParisiFinite.step_tendsto_coefficient_field line 397
  43. lemma OAI.ParisiFinite.dyadic_fixed_tendsto_coefficient line 430
  44. lemma OAI.ParisiFinite.dyadicEvolution_tendsto_coefficient line 448
  45. lemma OAI.ParisiFinite.field_tendsto_coefficient line 471
  46. lemma OAI.ParisiFinite.fieldGradient_tendsto_coefficient line 481
  47. lemma OAI.ParisiPath.drift_comp_tendsto line 532
  48. lemma OAI.ParisiPath.next_tendsto_drift line 548
  49. lemma OAI.ParisiPath.iterate_tendsto_drift line 581
  50. theorem OAI.ParisiPath.solution_tendsto_drift line 591
  51. lemma OAI.ParisiFinite.BoundedCoefficient.real_tendsto line 624
  52. lemma OAI.ParisiFinite.BoundedCoefficient.gradient_tendsto line 628
  53. lemma OAI.ParisiFinite.BoundedCoefficient.drift_tendsto line 634
  54. lemma OAI.ParisiFinite.BoundedCoefficient.feedback_solution_tendsto line 639
  55. lemma OAI.ParisiFinite.BoundedCoefficient.spin_tendsto line 644
  56. lemma OAI.ParisiFinite.BoundedCoefficient.expectedProduct_tendsto line 663