OAI/Probability/ParisiFinite/ContinuousTiltedMeanJoint.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Continuous Tilted Mean Joint.

  1. lemma OAI.ParisiFinite.continuous_tiltedMean_joint line 16
  2. lemma OAI.ParisiFinite.continuous_transform_val line 28
  3. lemma OAI.ParisiFinite.continuous_transform_d1 line 36
  4. lemma OAI.ParisiFinite.continuous_transform_d2 line 40
  5. lemma OAI.ParisiFinite.continuous_fieldOnInterval_val line 47
  6. lemma OAI.ParisiFinite.continuous_fieldOnInterval_d1 line 52
  7. lemma OAI.ParisiFinite.continuous_fieldOnInterval_d2 line 57
  8. def OAI.ParisiFinite.fieldOnInterval_dt line 64
  9. def OAI.ParisiFinite.fieldOnInterval_timeBound line 68
  10. lemma OAI.ParisiFinite.fieldOnInterval_dt_bound line 71
  11. lemma OAI.ParisiFinite.measurable_fieldOnInterval_dt line 90
  12. lemma OAI.ParisiFinite.continuous_fieldOnInterval_dt line 97
  13. lemma OAI.ParisiFinite.integrable_fieldOnInterval_dt line 105
  14. lemma OAI.ParisiFinite.fieldOnInterval_after line 112
  15. lemma OAI.ParisiFinite.fieldOnInterval_integral_before line 117
  16. lemma OAI.ParisiFinite.fieldOnInterval_integral_after line 130
  17. lemma OAI.ParisiFinite.fieldOnInterval_integral_time line 142