OAI/Probability/LogConcave/Numerics/MeanTree.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.LogConcaveSampling.MeanTree line 12
  2. def OAI.LogConcaveSampling.MeanTree.eval line 19
  3. def OAI.LogConcaveSampling.MeanTree.depth line 22
  4. def OAI.LogConcaveSampling.MeanTree.terms line 25
  5. def OAI.LogConcaveSampling.MeanTree.weight line 28
  6. def OAI.LogConcaveSampling.MeanTree.anchor line 31
  7. def OAI.LogConcaveSampling.MeanTree.zero line 34
  8. def OAI.LogConcaveSampling.MeanTree.scale line 36
  9. def OAI.LogConcaveSampling.MeanTree.add line 39
  10. def OAI.LogConcaveSampling.MeanTree.mean line 44
  11. theorem OAI.LogConcaveSampling.MeanTree.eval_anchor line 47
  12. theorem OAI.LogConcaveSampling.MeanTree.eval_zero line 49
  13. theorem OAI.LogConcaveSampling.MeanTree.eval_scale line 50
  14. theorem OAI.LogConcaveSampling.MeanTree.eval_add line 54
  15. theorem OAI.LogConcaveSampling.MeanTree.eval_mean line 59
  16. theorem OAI.LogConcaveSampling.MeanTree.depth_anchor line 63
  17. theorem OAI.LogConcaveSampling.MeanTree.depth_zero line 65
  18. theorem OAI.LogConcaveSampling.MeanTree.depth_scale line 66
  19. theorem OAI.LogConcaveSampling.MeanTree.depth_mean line 68
  20. theorem OAI.LogConcaveSampling.MeanTree.depth_add_le line 71
  21. def OAI.LogConcaveSampling.MeanTree.sumFin line 82
  22. lemma OAI.LogConcaveSampling.MeanTree.eval_sumFin line 86
  23. lemma OAI.LogConcaveSampling.MeanTree.depth_sumFin_le line 92
  24. def OAI.LogConcaveSampling.MeanTree.sumFamily line 98
  25. lemma OAI.LogConcaveSampling.MeanTree.eval_sumFamily line 101
  26. lemma OAI.LogConcaveSampling.MeanTree.depth_sumFamily_le line 106
  27. def OAI.LogConcaveSampling.MeanTree.conditional line 110
  28. lemma OAI.LogConcaveSampling.MeanTree.conditionalFieldMean_primitive line 113
  29. lemma OAI.LogConcaveSampling.MeanTree.eval_conditional line 126
  30. lemma OAI.LogConcaveSampling.MeanTree.depth_conditional_le line 132