OAI/Analysis/Steinitz/GaussianTail.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Scalar and matrix Gaussian tail estimates.

  1. lemma OAI.GaussianTail.integral_exp_square line 14
  2. lemma OAI.GaussianTail.integrable_exp_square line 30
  3. lemma OAI.GaussianTail.inverse_sqrt_one_sub_le_exp line 36
  4. lemma OAI.GaussianTail.quadratic_eigenbasis line 55
  5. lemma OAI.GaussianTail.quadratic_mgf_eq line 68
  6. lemma OAI.GaussianTail.quadratic_mgf_le line 87
  7. lemma OAI.GaussianTail.quadratic_mgf_integrable line 99
  8. lemma OAI.GaussianTail.quadratic_tail line 108
  9. lemma OAI.GaussianTail.eigenvalue_le_of_form_le line 136
  10. lemma OAI.GaussianTail.scaled_quadratic_tail line 148
  11. def OAI.GaussianTail.matrixMap line 195
  12. def OAI.GaussianTail.squareMass line 198
  13. lemma OAI.GaussianTail.squareMass_nonneg line 201
  14. lemma OAI.GaussianTail.gram_form line 204
  15. lemma OAI.GaussianTail.gram_trace line 211
  16. lemma OAI.GaussianTail.norm_sq_le_squareMass line 216
  17. lemma OAI.GaussianTail.matrix_square_tail line 223
  18. lemma OAI.GaussianTail.interpolated_form line 232
  19. lemma OAI.GaussianTail.interpolated_tail line 251