OAI/Probability/LogConcave/LowerBounds/WeightedEvaluation.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.LowerBound.weightedEvaluation line 24
  2. def OAI.LogConcaveSampling.LowerBound.spectralPowers line 29
  3. theorem OAI.LogConcaveSampling.LowerBound.spectral_power_span_eq_cosine_span line 35
  4. abbrev OAI.LogConcaveSampling.LowerBound.BlockIndex line 88
  5. def OAI.LogConcaveSampling.LowerBound.blockMatrix line 90
  6. def OAI.LogConcaveSampling.LowerBound.blockCoefficient line 93
  7. def OAI.LogConcaveSampling.LowerBound.blockLeft line 96
  8. def OAI.LogConcaveSampling.LowerBound.blockRight line 98
  9. theorem OAI.LogConcaveSampling.LowerBound.blockCoefficient_bound line 100
  10. theorem OAI.LogConcaveSampling.LowerBound.blockCoefficient_sum line 112
  11. theorem OAI.LogConcaveSampling.LowerBound.blockGram_entry line 131
  12. theorem OAI.LogConcaveSampling.LowerBound.blockWeightedGram_entry line 140
  13. theorem OAI.LogConcaveSampling.LowerBound.block_total_energy_eq line 150
  14. theorem OAI.LogConcaveSampling.LowerBound.block_total_energy_mean_le line 169
  15. def OAI.LogConcaveSampling.LowerBound.blockTolerance line 182
  16. theorem OAI.LogConcaveSampling.LowerBound.blockTolerance_pos line 184
  17. theorem OAI.LogConcaveSampling.LowerBound.block_good_event line 189
  18. def OAI.LogConcaveSampling.LowerBound.krylovSpace line 232
  19. theorem OAI.LogConcaveSampling.LowerBound.block_span_eq_krylov line 236
  20. theorem OAI.LogConcaveSampling.LowerBound.lower_span_statistic line 281
  21. def OAI.LogConcaveSampling.LowerBound.spectralDecay line 301
  22. theorem OAI.LogConcaveSampling.LowerBound.spectralDecay_pos line 303
  23. theorem OAI.LogConcaveSampling.LowerBound.spectralDecay_lt_one line 308
  24. theorem OAI.LogConcaveSampling.LowerBound.hasSum_geometric_cos line 313
  25. theorem OAI.LogConcaveSampling.LowerBound.reciprocal_spectrum_fourier line 341
  26. def OAI.LogConcaveSampling.LowerBound.cosineCorrelation line 384
  27. theorem OAI.LogConcaveSampling.LowerBound.cosineCorrelation_abs_le line 387
  28. theorem OAI.LogConcaveSampling.LowerBound.cosineCorrelation_diagonal line 401
  29. theorem OAI.LogConcaveSampling.LowerBound.cosineCorrelation_zero line 405
  30. theorem OAI.LogConcaveSampling.LowerBound.summable_weighted_cosineCorrelation line 408
  31. theorem OAI.LogConcaveSampling.LowerBound.reciprocal_spectrum_statistic_series line 420
  32. theorem OAI.LogConcaveSampling.LowerBound.reciprocal_spectrum_statistic_initial_sum line 466
  33. theorem OAI.LogConcaveSampling.LowerBound.reciprocal_spectrum_statistic_remainder line 476
  34. def OAI.LogConcaveSampling.LowerBound.targetVariance line 517
  35. theorem OAI.LogConcaveSampling.LowerBound.targetVariance_le_one line 520
  36. def OAI.LogConcaveSampling.LowerBound.targetGaussian line 524
  37. instance OAI.LogConcaveSampling.LowerBound.targetGaussian_probability line 527
  38. theorem OAI.LogConcaveSampling.LowerBound.targetGaussian_coordinate_law line 531
  39. def OAI.LogConcaveSampling.LowerBound.diagonalStatistic line 535
  40. theorem OAI.LogConcaveSampling.LowerBound.diagonalStatistic_memLp line 537
  41. theorem OAI.LogConcaveSampling.LowerBound.targetGaussian_statistic_mean line 543
  42. theorem OAI.LogConcaveSampling.LowerBound.targetGaussian_statistic_variance line 553
  43. theorem OAI.LogConcaveSampling.LowerBound.targetGaussian_statistic_variance_le line 568
  44. theorem OAI.LogConcaveSampling.LowerBound.targetGaussian_norm_mean_le line 584
  45. theorem OAI.LogConcaveSampling.LowerBound.lower_target_statistic line 596
  46. theorem OAI.LogConcaveSampling.LowerBound.real_chebyshev line 609
  47. def OAI.LogConcaveSampling.LowerBound.separationThreshold line 617
  48. def OAI.LogConcaveSampling.LowerBound.separationEvent line 619
  49. theorem OAI.LogConcaveSampling.LowerBound.separationEvent_measurable line 623
  50. theorem OAI.LogConcaveSampling.LowerBound.target_separation_tail line 630