OAI/Probability/FreeIsing/Stochastic/RandomRiemannCompensator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.RandomRiemann.partitionSum line 12
  2. theorem OAI.Problem367.RandomRiemann.abs_partitionSum_le line 15
  3. theorem OAI.Problem367.RandomRiemann.partition_error_le line 29
  4. def OAI.Problem367.RandomRiemann.stoppedPoint line 58
  5. def OAI.Problem367.RandomRiemann.stoppedSum line 60
  6. theorem OAI.Problem367.RandomRiemann.stoppedPoint_mono line 64
  7. theorem OAI.Problem367.RandomRiemann.stoppedPoint_zero line 68
  8. theorem OAI.Problem367.RandomRiemann.stoppedPoint_end line 71
  9. theorem OAI.Problem367.RandomRiemann.stoppedPoint_step_le line 74
  10. theorem OAI.Problem367.RandomRiemann.stoppedSum_eq_partitionSum line 86
  11. theorem OAI.Problem367.RandomRiemann.abs_stoppedSum_le line 97
  12. theorem OAI.Problem367.RandomRiemann.tendsto_stoppedSum line 108
  13. theorem OAI.Problem367.RandomRiemann.tendsto_stoppedSum_L1 line 154
  14. theorem OAI.Problem367.RandomRiemann.tendsto_stoppedSquareSum_L1 line 183
  15. theorem OAI.Problem367.RandomRiemann.tendsto_stoppedSquareSum_L1_nnreal line 199