OAI/Probability/SpanningForest/Picard.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.Picard.iterate line 14
  2. def OAI.Problem336.Picard.majorant line 20
  3. lemma OAI.Problem336.Picard.intervalIntegrable_of_measurable_bounded line 23
  4. lemma OAI.Problem336.Picard.continuous_iterate line 32
  5. lemma OAI.Problem336.Picard.majorant_nonneg line 48
  6. lemma OAI.Problem336.Picard.continuous_majorant line 53
  7. lemma OAI.Problem336.Picard.integral_majorant line 57
  8. lemma OAI.Problem336.Picard.measurable_drift_iterate line 69
  9. lemma OAI.Problem336.Picard.intervalIntegrable_drift_iterate line 77
  10. lemma OAI.Problem336.Picard.iterate_increment_le line 86
  11. lemma OAI.Problem336.Picard.measurable_parametric_intervalIntegral line 131
  12. lemma OAI.Problem336.Picard.measurable_iterate line 151
  13. def OAI.Problem336.Picard.decode line 172
  14. lemma OAI.Problem336.Picard.measurable_decode line 175
  15. lemma OAI.Problem336.Picard.iterate_relabel line 185
  16. lemma OAI.Problem336.Picard.decode_relabel line 209
  17. lemma OAI.Problem336.Picard.iterate_causal line 222
  18. lemma OAI.Problem336.Picard.decode_causal line 242