OAI/Probability/FreeIsing/Martingales/PredictableMeshApproximation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.PredictableMesh.point line 12
  2. def OAI.Problem367.PredictableMesh.left line 14
  3. theorem OAI.Problem367.PredictableMesh.point_zero line 17
  4. theorem OAI.Problem367.PredictableMesh.left_zero line 19
  5. theorem OAI.Problem367.PredictableMesh.point_strictMono line 21
  6. theorem OAI.Problem367.PredictableMesh.left_eq_of_mem_Ioc line 25
  7. theorem OAI.Problem367.PredictableMesh.mem_mesh_Ioc line 39
  8. theorem OAI.Problem367.PredictableMesh.left_le line 54
  9. theorem OAI.Problem367.PredictableMesh.le_left_add_width line 59
  10. theorem OAI.Problem367.PredictableMesh.tendsto_left line 66
  11. theorem OAI.Problem367.PredictableMesh.measurable_left line 79
  12. def OAI.Problem367.PredictableMesh.sample line 83
  13. theorem OAI.Problem367.PredictableMesh.sample_tendsto line 86
  14. theorem OAI.Problem367.PredictableMesh.sample_stronglyAdapted line 91
  15. theorem OAI.Problem367.PredictableMesh.sample_isStronglyPredictable line 96
  16. theorem OAI.Problem367.PredictableMesh.isStronglyPredictable_of_continuous line 122
  17. theorem OAI.Problem367.PredictableMesh.stronglyMeasurable_uncurry line 130
  18. theorem OAI.Problem367.PredictableMesh.stronglyMeasurable_sample line 137
  19. theorem OAI.Problem367.PredictableMesh.memLp_uncurry line 144
  20. theorem OAI.Problem367.PredictableMesh.memLp_sample line 153
  21. theorem OAI.Problem367.PredictableMesh.tendsto_integral_sq_sample_sub line 163
  22. theorem OAI.Problem367.PredictableMesh.tendsto_time_integral_sq_sample_sub line 198