OAI/Probability/FreeIsing/Estimates/CharacteristicRecurrence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ExponentialTaylor.norm_gaussian_recurrence_error_le_sum line 12
  2. theorem OAI.Problem367.ExponentialTaylor.eq_gaussian_mul_of_recurrence_errors_tendsto_zero line 26
  3. theorem OAI.Problem367.ExponentialTaylor.sum_mul_sqrt_le_total_mul_sqrt_mesh line 46
  4. theorem OAI.Problem367.ExponentialTaylor.sum_sq_le_total_mul_mesh line 57
  5. theorem OAI.Problem367.ExponentialTaylor.sum_cube_le_total_mul_mesh_sq line 68
  6. theorem OAI.Problem367.ExponentialTaylor.tendsto_sum_brownian_drift_errors line 81
  7. theorem OAI.Problem367.ExponentialTaylor.eq_gaussian_mul_of_local_error line 118
  8. theorem OAI.Problem367.ExponentialTaylor.eq_gaussian_mul_of_local_error_nnreal line 162