OAI/Probability/LogConcave/TensorGraphs/HessianIncidenceTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.AdjointRemoval.hessian_congr_on_tokens line 22
2. def OAI.LogConcaveSampling.AdjointRemoval.hessianIncidenceTensor line 38
3. lemma OAI.LogConcaveSampling.AdjointRemoval.hessianIncidenceTensor_global line 48
4. abbrev OAI.LogConcaveSampling.AdjointRemoval.TraceEdge line 69
5. def OAI.LogConcaveSampling.AdjointRemoval.traceEmbed line 72
6. abbrev OAI.LogConcaveSampling.AdjointRemoval.PrimaryTraceSlot line 76
7. def OAI.LogConcaveSampling.AdjointRemoval.primaryIncidenceTensor line 83
8. lemma OAI.LogConcaveSampling.AdjointRemoval.primaryIncidenceTensor_global line 95
9. def OAI.LogConcaveSampling.AdjointRemoval.branchIncidenceTensor line 122
10. lemma OAI.LogConcaveSampling.AdjointRemoval.branchIncidenceTensor_global line 134
11. theorem OAI.LogConcaveSampling.AdjointRemoval.literal_branch_integral_bound line 151
12. def OAI.LogConcaveSampling.AdjointRemoval.primaryIncidentCases line 184
13. def OAI.LogConcaveSampling.AdjointRemoval.primarySlotEquiv line 221
14. lemma OAI.LogConcaveSampling.AdjointRemoval.primarySlotEquiv_trace line 231
15. lemma OAI.LogConcaveSampling.AdjointRemoval.primarySlotEquiv_source line 236
16. lemma OAI.LogConcaveSampling.AdjointRemoval.primarySlotEquiv_derivative line 241