OAI/Probability/LogConcave/Numerics/ChildNoise.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.MeanTree.childNoise line 16
  2. def OAI.LogConcaveSampling.MeanTree.reserve line 18
  3. def OAI.LogConcaveSampling.MeanTree.compileTerms line 21
  4. def OAI.LogConcaveSampling.MeanTree.compile line 29
  5. def OAI.LogConcaveSampling.MeanTree.compileRoot line 35
  6. lemma OAI.LogConcaveSampling.MeanTree.calls_compileTerms line 42
  7. lemma OAI.LogConcaveSampling.MeanTree.slots_compileTerms line 51
  8. lemma OAI.LogConcaveSampling.MeanTree.calls_compile line 60
  9. lemma OAI.LogConcaveSampling.MeanTree.slots_compile line 67
  10. theorem OAI.LogConcaveSampling.MeanTree.compile_query_cap line 74
  11. lemma OAI.LogConcaveSampling.MeanTree.coefficient_energy line 92
  12. lemma OAI.LogConcaveSampling.MeanTree.childNoise_energy line 97
  13. lemma OAI.LogConcaveSampling.MeanTree.reserve_nonneg line 108
  14. lemma OAI.LogConcaveSampling.MeanTree.reserve_variance line 111
  15. lemma OAI.LogConcaveSampling.MeanTree.reserve_positive line 117
  16. theorem OAI.LogConcaveSampling.MeanTree.weighted_gaussian_law line 127
  17. theorem OAI.LogConcaveSampling.MeanTree.reserve_gaussian_law line 154
  18. def OAI.LogConcaveSampling.MeanTree.declaredNoise line 184
  19. def OAI.LogConcaveSampling.MeanTree.declaredReserve line 185
  20. def OAI.LogConcaveSampling.MeanTree.compileDeclared line 188
  21. def OAI.LogConcaveSampling.MeanTree.compileDeclaredRoot line 194
  22. lemma OAI.LogConcaveSampling.MeanTree.declaredNoise_energy line 200
  23. lemma OAI.LogConcaveSampling.MeanTree.declaredReserve_variance line 209
  24. lemma OAI.LogConcaveSampling.MeanTree.declaredReserve_positive line 216
  25. lemma OAI.LogConcaveSampling.MeanTree.calls_compileDeclared line 222
  26. theorem OAI.LogConcaveSampling.MeanTree.compileDeclared_program line 229