OAI/Probability/FreeIsing/Martingales/StrongMaximal.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.MartingaleStrongMaximal.runningMax line 13
  2. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_zero line 17
  3. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_succ line 19
  4. theorem OAI.Problem367.MartingaleStrongMaximal.self_le_runningMax line 22
  5. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_mono line 27
  6. theorem OAI.Problem367.MartingaleStrongMaximal.le_runningMax line 32
  7. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_sq_le_twice line 35
  8. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_sq_le_four line 50
  9. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_memLp line 58
  10. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_stronglyAdapted line 64
  11. theorem OAI.Problem367.MartingaleStrongMaximal.integral_mul_sub_nonneg line 76
  12. theorem OAI.Problem367.MartingaleStrongMaximal.finite_submartingale_maximal_sq line 91
  13. theorem OAI.Problem367.MartingaleStrongMaximal.submartingale_abs line 120
  14. theorem OAI.Problem367.MartingaleStrongMaximal.finite_martingale_maximal_sq line 129
  15. theorem OAI.Problem367.MartingaleStrongMaximal.runningMax_le line 137
  16. theorem OAI.Problem367.MartingaleStrongMaximal.sampled_martingale_maximal_sq line 144
  17. def OAI.Problem367.MartingaleStrongMaximal.dyadicPoint line 158
  18. def OAI.Problem367.MartingaleStrongMaximal.dyadicCount line 160
  19. theorem OAI.Problem367.MartingaleStrongMaximal.dyadicPoint_mono line 162
  20. theorem OAI.Problem367.MartingaleStrongMaximal.dyadicPoint_double line 167
  21. theorem OAI.Problem367.MartingaleStrongMaximal.dyadicPoint_le_iff line 172
  22. theorem OAI.Problem367.MartingaleStrongMaximal.dyadicPoint_eq_mesh line 178
  23. def OAI.Problem367.MartingaleStrongMaximal.gridMax line 183
  24. theorem OAI.Problem367.MartingaleStrongMaximal.gridMax_nonneg line 187
  25. theorem OAI.Problem367.MartingaleStrongMaximal.gridMax_mono line 193
  26. theorem OAI.Problem367.MartingaleStrongMaximal.gridMax_memLp line 206
  27. theorem OAI.Problem367.MartingaleStrongMaximal.gridMax_integral_sq_le line 210
  28. def OAI.Problem367.MartingaleStrongMaximal.supremumSq line 217
  29. theorem OAI.Problem367.MartingaleStrongMaximal.supremumSq_eq_iSup_gridMax line 222
  30. theorem OAI.Problem367.MartingaleStrongMaximal.continuous_martingale_maximal_sq line 270
  31. theorem OAI.Problem367.MartingaleStrongMaximal.supremumSq_aemeasurable line 292
  32. theorem OAI.Problem367.MartingaleStrongMaximal.ae_supremumSq_lt_top line 304
  33. def OAI.Problem367.MartingaleStrongMaximal.maximalSquare line 312
  34. theorem OAI.Problem367.MartingaleStrongMaximal.integrable_maximalSquare line 315
  35. theorem OAI.Problem367.MartingaleStrongMaximal.integral_maximalSquare_le line 323
  36. theorem OAI.Problem367.MartingaleStrongMaximal.tendsto_integral_maximalSquare_sub line 335
  37. theorem OAI.Problem367.MartingaleStrongMaximal.ae_all_sq_le_maximalSquare line 353