OAI/Probability/LogConcave/Complexity/KernelActionNormalizedBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.circuitD_dimension line 12
  2. lemma OAI.LogConcaveSampling.harmonicNormalizedTerm_mono line 17
  3. lemma OAI.LogConcaveSampling.kernelNormalizedTerm_mono line 23
  4. lemma OAI.LogConcaveSampling.weighted_uniform_upper line 31
  5. def OAI.LogConcaveSampling.kernelActionNormalizedBudget line 37
  6. lemma OAI.LogConcaveSampling.kernelActionNormalizedBudget_nonneg line 45
  7. theorem OAI.LogConcaveSampling.kernelActionRmsBudget_normalized line 50