OAI/Probability/LogConcave/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Subpolynomial upper bounds and logarithmic lower bounds for exact first-order sampling, with optimal dimension exponent zero.

  1. lemma OAI.LogConcaveSampling.CanSample.queryComplexity_le line 28
  2. theorem OAI.LogConcaveSampling.source_subpolynomial_upper line 33
  3. theorem OAI.LogConcaveSampling.source_exponent_zero line 54
  4. theorem OAI.LogConcaveSampling.source_gammaStar_zero line 63
  5. theorem OAI.LogConcaveSampling.exact_source_main line 68

    Distinct definitions of this name: ComparatorChallenges/LogConcaveQuery.lean:81 (same statement text; different proof or body). Qualify references as OAI.LogConcaveSampling.exact_source_main@path.