OAI/Probability/FreeIsing/Estimates/ArtanhTaylor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.ArtanhTaylor.denominator_pos line 12
  2. theorem OAI.Problem367.ArtanhTaylor.contDiffAt_artanh line 16
  3. lemma OAI.Problem367.ArtanhTaylor.hasDerivAt_first line 26
  4. lemma OAI.Problem367.ArtanhTaylor.hasDerivAt_second line 35
  5. lemma OAI.Problem367.ArtanhTaylor.iteratedDeriv_two line 46
  6. lemma OAI.Problem367.ArtanhTaylor.iteratedDeriv_three line 54
  7. theorem OAI.Problem367.ArtanhTaylor.abs_iteratedDeriv_three_le line 63
  8. theorem OAI.Problem367.ArtanhTaylor.abs_remainder_le line 81
  9. def OAI.Problem367.ArtanhTaylor.remainder line 130
  10. theorem OAI.Problem367.ArtanhTaylor.sum_remainder line 134
  11. theorem OAI.Problem367.ArtanhTaylor.abs_sum_remainder_le line 148
  12. theorem OAI.Problem367.ArtanhTaylor.tendsto_sum_remainder line 174
  13. lemma OAI.Problem367.ArtanhTaylor.measurable_remainder line 197
  14. theorem OAI.Problem367.ArtanhTaylor.integrable_sum_remainder_and_bound line 202
  15. theorem OAI.Problem367.ArtanhTaylor.integrable_cube_of_localized line 242
  16. theorem OAI.Problem367.ArtanhTaylor.tendsto_integral_abs_sum_remainder line 255