OAI/Probability/LogConcave/LowerBounds/Theta.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.LowerBound.roundGaussianPair_law line 21
  2. lemma OAI.LogConcaveSampling.LowerBound.roundTapeColumns_law line 26
  3. theorem OAI.LogConcaveSampling.LowerBound.couplingColumns_law line 44
  4. def OAI.LogConcaveSampling.LowerBound.theta line 67
  5. def OAI.LogConcaveSampling.LowerBound.eigenvalue line 69
  6. def OAI.LogConcaveSampling.LowerBound.weight line 71
  7. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_eq_zero line 73
  8. theorem OAI.LogConcaveSampling.LowerBound.eigenvalue_bounds line 106
  9. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_sq line 111
  10. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_mul_of_lt line 124
  11. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_mul line 143
  12. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_triple_of_le line 150
  13. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_triple line 174
  14. theorem OAI.LogConcaveSampling.LowerBound.sum_half_grid_cos_sq_ite line 191
  15. def OAI.LogConcaveSampling.LowerBound.cosineAmplitude line 213
  16. theorem OAI.LogConcaveSampling.LowerBound.cosineAmplitude_pos line 215
  17. theorem OAI.LogConcaveSampling.LowerBound.cosineAmplitude_sq_le_two line 219
  18. def OAI.LogConcaveSampling.LowerBound.cosineColumn line 223
  19. theorem OAI.LogConcaveSampling.LowerBound.cosineColumn_orthonormal line 226
  20. theorem OAI.LogConcaveSampling.LowerBound.cosineColumn_sq_le line 253
  21. theorem OAI.LogConcaveSampling.LowerBound.cosineColumn_product_le line 267
  22. theorem OAI.LogConcaveSampling.LowerBound.cosineColumn_weighted_orthogonal line 275
  23. theorem OAI.LogConcaveSampling.LowerBound.integral_pow_four_gaussianReal line 296
  24. theorem OAI.LogConcaveSampling.LowerBound.integral_pow_two_gaussianReal line 332
  25. theorem OAI.LogConcaveSampling.LowerBound.holder_four_four_two line 338
  26. theorem OAI.LogConcaveSampling.LowerBound.gaussian_memLp line 349
  27. theorem OAI.LogConcaveSampling.LowerBound.gaussian_integral_sq line 355
  28. theorem OAI.LogConcaveSampling.LowerBound.gaussian_integral_fourth line 361
  29. theorem OAI.LogConcaveSampling.LowerBound.gaussian_sq_memLp line 367
  30. theorem OAI.LogConcaveSampling.LowerBound.gaussian_sq_variance line 374
  31. theorem OAI.LogConcaveSampling.LowerBound.independent_gaussian_product_variance line 382
  32. def OAI.LogConcaveSampling.LowerBound.gaussianRow line 408
  33. instance OAI.LogConcaveSampling.LowerBound.gaussianRow_probability line 411
  34. def OAI.LogConcaveSampling.LowerBound.gaussianRows line 415
  35. instance OAI.LogConcaveSampling.LowerBound.gaussianRows_probability line 418
  36. theorem OAI.LogConcaveSampling.LowerBound.gaussianRow_coordinate_law line 422
  37. theorem OAI.LogConcaveSampling.LowerBound.gaussianRow_coordinates_independent line 426
  38. theorem OAI.LogConcaveSampling.LowerBound.gaussianRow_product_memLp line 430
  39. theorem OAI.LogConcaveSampling.LowerBound.gaussianRow_product_mean line 439
  40. theorem OAI.LogConcaveSampling.LowerBound.gaussianRow_product_variance line 450
  41. def OAI.LogConcaveSampling.LowerBound.gaussianRowSum line 460
  42. theorem OAI.LogConcaveSampling.LowerBound.gaussianRowSum_memLp line 463
  43. theorem OAI.LogConcaveSampling.LowerBound.gaussianRowSum_mean line 470
  44. theorem OAI.LogConcaveSampling.LowerBound.gaussianRowSum_variance line 491
  45. theorem OAI.LogConcaveSampling.LowerBound.gaussianRowSum_variance_le line 504
  46. def OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy line 528
  47. theorem OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy_nonneg line 533
  48. theorem OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy_measurable line 538
  49. theorem OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy_integrable line 543
  50. theorem OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy_mean line 550
  51. theorem OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy_mean_le line 563
  52. theorem OAI.LogConcaveSampling.LowerBound.rowDeviationEnergy_tail line 574
  53. def OAI.LogConcaveSampling.LowerBound.matrixEnergy line 593
  54. theorem OAI.LogConcaveSampling.LowerBound.matrixEnergy_nonneg line 596
  55. theorem OAI.LogConcaveSampling.LowerBound.quadratic_form_bound_of_energy line 600
  56. theorem OAI.LogConcaveSampling.LowerBound.gram_control_on_column_span line 629