OAI/Probability/FreeIsing/Brownian/ContinuousAssociativity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.BrownianIntegralProcess.stopped_sum_at_grid line 15
  2. theorem OAI.Problem367.BrownianIntegralProcess.stoppedUniformSum_at_grid line 38
  3. def OAI.Problem367.BrownianContinuousAssociativity.mixedSum line 54
  4. theorem OAI.Problem367.BrownianContinuousAssociativity.mixedSum_difference_bound line 59
  5. theorem OAI.Problem367.BrownianContinuousAssociativity.mixedSum_difference_tendsto line 112
  6. theorem OAI.Problem367.BrownianContinuousAssociativity.uniformSum_stoppedUniformSum_eq_mixedSum line 152
  7. theorem OAI.Problem367.BrownianContinuousAssociativity.uniformSum_memLp line 174
  8. theorem OAI.Problem367.BrownianContinuousAssociativity.mixedSum_outer_difference_tendsto line 182
  9. theorem OAI.Problem367.BrownianContinuousAssociativity.mixedSum_memLp line 235
  10. theorem OAI.Problem367.BrownianContinuousAssociativity.uniformSum_associativity line 253
  11. theorem OAI.Problem367.BrownianContinuousAssociativity.exists_terminal_associative_integral line 305