OAI/Probability/LogConcave/LowerBounds/SpectrumOperator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.LowerBound.diagonalStatistic_eq_dotProduct line 24
  2. theorem OAI.LogConcaveSampling.LowerBound.normStatistic_eq_dotProduct line 31
  3. theorem OAI.LogConcaveSampling.LowerBound.separationThreshold_eq line 35
  4. theorem OAI.LogConcaveSampling.LowerBound.algorithm_span_separation_bound line 44
  5. def OAI.LogConcaveSampling.LowerBound.spectrumOperator line 80
  6. theorem OAI.LogConcaveSampling.LowerBound.spectrumOperator_apply line 83
  7. def OAI.LogConcaveSampling.LowerBound.quadraticOperator line 88
  8. def OAI.LogConcaveSampling.LowerBound.quadraticPotential line 92
  9. lemma OAI.LogConcaveSampling.LowerBound.spectrumOperator_symmetric line 95
  10. lemma OAI.LogConcaveSampling.LowerBound.quadraticOperator_symmetric line 104
  11. lemma OAI.LogConcaveSampling.LowerBound.quadraticOperator_bounds line 113
  12. lemma OAI.LogConcaveSampling.LowerBound.quadraticPotential_hasGradientAt line 141
  13. theorem OAI.LogConcaveSampling.LowerBound.quadraticPotential_gradient line 157
  14. theorem OAI.LogConcaveSampling.LowerBound.quadraticPotential_admissible line 161
  15. theorem OAI.LogConcaveSampling.LowerBound.quadratic_firstOrderReply line 171