OAI/Probability/SKGap/Gaussian/SquaredGaussianFourth.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGapCutoff.RandomMatrix.matrix_opNorm_sq_le_frobenius line 41
  2. lemma OAI.SKGapCutoff.RandomMatrix.matrix_fourth_trace_bound line 58
  3. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_sq_integral line 81
  4. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_squared_centered_integral line 86
  5. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_squared_centered_memLp_four line 95
  6. def OAI.SKGapCutoff.RandomMatrix.squaredGaussianFourth line 102
  7. lemma OAI.SKGapCutoff.RandomMatrix.squaredGaussianFourth_nonneg line 104
  8. lemma OAI.SKGapCutoff.RandomMatrix.gaussian_squared_fourth_integral line 109
  9. def OAI.SKGapCutoff.RandomMatrix.centeredSquareCoordinate line 125
  10. def OAI.SKGapCutoff.RandomMatrix.centeredSquared line 127
  11. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_diag line 130
  12. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_symm line 133
  13. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquareCoordinate_memLp line 137
  14. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquareCoordinate_mean line 142
  15. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquareCoordinate_fourth line 149
  16. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquareCoordinate_independent line 157
  17. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_memLp line 162
  18. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_fourth_integrable line 170
  19. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_fourth_le line 176
  20. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_cyclic_integrable line 185
  21. lemma OAI.SKGapCutoff.RandomMatrix.minmax_eq_iff line 197
  22. lemma OAI.SKGapCutoff.RandomMatrix.integral_sq_mul_sq_le_fourth line 223
  23. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_cyclic_zero line 235
  24. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_cyclic_le line 274
  25. def OAI.SKGapCutoff.RandomMatrix.squaredFourthTrace line 315
  26. lemma OAI.SKGapCutoff.RandomMatrix.squaredFourthTrace_integrable line 319
  27. lemma OAI.SKGapCutoff.RandomMatrix.squaredFourthTrace_nonneg line 326
  28. lemma OAI.SKGapCutoff.RandomMatrix.squaredFourthTrace_integral_le line 330
  29. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_opNorm_tail line 354
  30. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_disorder_tail line 367
  31. lemma OAI.SKGapCutoff.RandomMatrix.centeredSquared_disorder_tendsto line 376
  32. def OAI.SKGapCutoff.RandomMatrix.sampledSquaredDeviation line 387
  33. lemma OAI.SKGapCutoff.RandomMatrix.sampledSquaredDeviation_eq line 390
  34. lemma OAI.SKGapCutoff.RandomMatrix.sampledSquaredDeviation_norm_le line 403
  35. lemma OAI.SKGapCutoff.RandomMatrix.sampledSquaredDeviation_tendsto line 418