OAI/Probability/FreeIsing/Martingales/TaylorRemainder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.MartingaleTaylorRemainder.cubic_le_quadratic_add_quartic line 14
2. theorem OAI.Problem367.MartingaleTaylorRemainder.integrable_abs_cube line 31
3. theorem OAI.Problem367.MartingaleTaylorRemainder.integral_sum_abs_cube_le line 42
4. theorem OAI.Problem367.MartingaleTaylorRemainder.tendsto_zero_of_young_bound line 64
5. theorem OAI.Problem367.MartingaleTaylorRemainder.tendsto_integral_sum_abs_cube_zero line 89
6. theorem OAI.Problem367.MartingaleTaylorRemainder.remainder_L1_of_cubic_bound line 113
7. theorem OAI.Problem367.MartingaleTaylorRemainder.ae_eq_add_of_taylor_L1_limits line 140