OAI/Probability/LogConcave/TensorGraphs/Inside.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.AdjointRemoval.inside line 25
2. def OAI.LogConcaveSampling.AdjointRemoval.primary line 28
3. def OAI.LogConcaveSampling.AdjointRemoval.hessian line 32
4. def OAI.LogConcaveSampling.AdjointRemoval.term line 35
5. lemma OAI.LogConcaveSampling.AdjointRemoval.hessian_hit line 40
6. lemma OAI.LogConcaveSampling.AdjointRemoval.term_split line 43
7. lemma OAI.LogConcaveSampling.AdjointRemoval.primary_congr line 52
8. lemma OAI.LogConcaveSampling.AdjointRemoval.hitPrimary_term line 65
9. lemma OAI.LogConcaveSampling.AdjointRemoval.pair_term line 97
10. lemma OAI.LogConcaveSampling.AdjointRemoval.hitHessian_term line 121
11. structure OAI.LogConcaveSampling.AdjointRemoval.Regular line 141
12. lemma OAI.LogConcaveSampling.AdjointRemoval.Regular.primary_polyC1 line 151
13. lemma OAI.LogConcaveSampling.AdjointRemoval.Regular.term_polyC1 line 159
14. lemma OAI.LogConcaveSampling.AdjointRemoval.Regular.integrable_term line 164
15. lemma OAI.LogConcaveSampling.AdjointRemoval.primary_directional line 169
16. lemma OAI.LogConcaveSampling.AdjointRemoval.primary_branch_integrand line 186
17. lemma OAI.LogConcaveSampling.AdjointRemoval.pending_sum line 198
18. theorem OAI.LogConcaveSampling.AdjointRemoval.integral_one_step line 205
19. lemma OAI.LogConcaveSampling.AdjointRemoval.list_sum_map_flatMap line 261
20. theorem OAI.LogConcaveSampling.AdjointRemoval.integral_expand line 268
21. lemma OAI.LogConcaveSampling.AdjointRemoval.term_terminal line 284
22. theorem OAI.LogConcaveSampling.AdjointRemoval.actual_adjoint_expansion line 291
23. lemma OAI.LogConcaveSampling.AdjointRemoval.product_tensorAdjoint line 314
24. theorem OAI.LogConcaveSampling.AdjointRemoval.tensor_actual_adjoint_expansion line 323
25. theorem OAI.LogConcaveSampling.AdjointRemoval.tensor_actual_adjoint_expansion_branch_first line 344