OAI/Probability/FreeIsing/Martingales/BoundedMartingaleVariation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.BoundedMartingaleVariation.bounded_pow_memLp_two line 14
  2. theorem OAI.Problem367.BoundedMartingaleVariation.sum_sq_increment line 23
  3. theorem OAI.Problem367.BoundedMartingaleVariation.sq_sum_sq_increment_le line 32
  4. theorem OAI.Problem367.BoundedMartingaleVariation.integral_sq_quadratic_variation_le line 47
  5. def OAI.Problem367.BoundedMartingaleVariation.incrementModulus line 112
  6. theorem OAI.Problem367.BoundedMartingaleVariation.incrementModulus_nonneg line 115
  7. theorem OAI.Problem367.BoundedMartingaleVariation.abs_increment_le_modulus line 118
  8. theorem OAI.Problem367.BoundedMartingaleVariation.incrementModulus_le line 123
  9. theorem OAI.Problem367.BoundedMartingaleVariation.stronglyMeasurable_incrementModulus line 131
  10. theorem OAI.Problem367.BoundedMartingaleVariation.tendsto_incrementModulus_of_uniformContinuousOn line 143
  11. theorem OAI.Problem367.BoundedMartingaleVariation.mul_le_young line 168
  12. theorem OAI.Problem367.BoundedMartingaleVariation.tendsto_integral_sum_fourth_of_modulus line 181
  13. theorem OAI.Problem367.BoundedMartingaleVariation.tendsto_integral_sum_fourth_of_continuous line 261
  14. theorem OAI.Problem367.BoundedMartingaleVariation.tendsto_sum_integral_fourth_of_continuous line 282
  15. theorem OAI.Problem367.BoundedMartingaleVariation.integral_quadratic_variation_le line 305