OAI/Probability/LogConcave/Sampling/ProbabilityNormalizedTerm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.kernel_error_factor line 12
  2. def OAI.LogConcaveSampling.probabilityNormalizedTerm line 30
  3. lemma OAI.LogConcaveSampling.probabilityNormalizedTerm_nonneg line 33
  4. lemma OAI.LogConcaveSampling.probabilityRmsBudget_normalized line 39
  5. def OAI.LogConcaveSampling.harmonicNormalizedTerm line 55
  6. lemma OAI.LogConcaveSampling.harmonicNormalizedTerm_nonneg line 58
  7. lemma OAI.LogConcaveSampling.harmonicRmsBudget_normalized line 61
  8. def OAI.LogConcaveSampling.numericalContractionCoefficient line 114
  9. def OAI.LogConcaveSampling.numericalErrorCoefficient line 116
  10. def OAI.LogConcaveSampling.kernelNormalizedTerm line 119
  11. lemma OAI.LogConcaveSampling.numericalContractionCoefficient_pos line 124
  12. lemma OAI.LogConcaveSampling.numericalErrorCoefficient_pos line 128
  13. lemma OAI.LogConcaveSampling.numericalContraction_bound line 132
  14. theorem OAI.LogConcaveSampling.kernelValueRmsBudget_normalized line 150