OAI/Probability/FreeIsing/Martingales/StoppedProcessTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.StoppedProcessTransport.stoppedProcess_pullback line 14
  2. theorem OAI.Problem367.StoppedProcessTransport.stoppedValue_pullback line 19
  3. theorem OAI.Problem367.StoppedProcessTransport.isStoppingTime_pullback line 23
  4. theorem OAI.Problem367.StoppedProcessTransport.stoppedValue_ae_eq_of_continuous line 32
  5. theorem OAI.Problem367.StoppedProcessTransport.stoppedProcess_ae_eq_of_continuous line 44
  6. theorem OAI.Problem367.StoppedProcessTransport.integral_stoppedProcess_sq_pullback line 58
  7. theorem OAI.Problem367.StoppedProcessTransport.integral_stoppedProcess_sq_congr line 73
  8. theorem OAI.Problem367.StoppedProcessTransport.integral_before_stop_pullback line 86
  9. theorem OAI.Problem367.StoppedProcessTransport.intervalIntegral_before_stop_pullback line 106
  10. theorem OAI.Problem367.StoppedProcessTransport.local_square_identity_congr line 121