OAI/Probability/FreeIsing/Martingales/ArtanhMartingaleFormula.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ArtanhMartingaleFormula.firstWeight line 21
  2. def OAI.Problem367.ArtanhMartingaleFormula.secondWeight line 22
  3. def OAI.Problem367.ArtanhMartingaleFormula.linearSum line 24
  4. def OAI.Problem367.ArtanhMartingaleFormula.quadraticSum line 27
  5. def OAI.Problem367.ArtanhMartingaleFormula.compensatorSum line 30
  6. lemma OAI.Problem367.ArtanhMartingaleFormula.firstWeight_bound line 33
  7. lemma OAI.Problem367.ArtanhMartingaleFormula.secondWeight_bound line 42
  8. lemma OAI.Problem367.ArtanhMartingaleFormula.stronglyMeasurable_firstWeight line 53
  9. lemma OAI.Problem367.ArtanhMartingaleFormula.stronglyMeasurable_secondWeight line 59
  10. theorem OAI.Problem367.ArtanhMartingaleFormula.tendsto_integral_abs_zero_of_sq line 64
  11. theorem OAI.Problem367.ArtanhMartingaleFormula.taylor_identity line 74
  12. theorem OAI.Problem367.ArtanhMartingaleFormula.quadratic_sub_compensator line 94
  13. lemma OAI.Problem367.ArtanhMartingaleFormula.tendsto_L1_of_intermediate line 105
  14. theorem OAI.Problem367.ArtanhMartingaleFormula.artanh_eq_of_cubic_and_compensated_limits line 123
  15. theorem OAI.Problem367.ArtanhMartingaleFormula.integral_grid_square_sum_le line 210
  16. theorem OAI.Problem367.ArtanhMartingaleFormula.artanh_eq_of_compensated_sum_limits line 233
  17. theorem OAI.Problem367.ArtanhMartingaleFormula.artanh_eq_of_continuous_compensated_limits line 291
  18. theorem OAI.Problem367.ArtanhMartingaleFormula.artanh_eq_stochasticLimit_add_integral line 368