OAI/Probability/LogConcave/TensorGraphs/PrimaryPositionTensor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.AdjointRemoval.primaryPositionTensor line 27
2. lemma OAI.LogConcaveSampling.AdjointRemoval.primaryIncidenceTensor_positions line 36
3. lemma OAI.LogConcaveSampling.AdjointRemoval.primaryIncidenceTensor_allSplit line 55
4. def OAI.LogConcaveSampling.AdjointRemoval.hessianPositionList line 73
5. def OAI.LogConcaveSampling.AdjointRemoval.hessianPositionTensor line 76
6. lemma OAI.LogConcaveSampling.AdjointRemoval.hessianIncidence_direction line 83
7. lemma OAI.LogConcaveSampling.AdjointRemoval.hessianIncidenceTensor_positions line 98
8. lemma OAI.LogConcaveSampling.AdjointRemoval.hessianIncidenceTensor_allSplit line 121
9. theorem OAI.LogConcaveSampling.AdjointRemoval.positional_branch_integral_bound line 144
10. lemma OAI.LogConcaveSampling.AdjointRemoval.hessian_sum_toType line 177
11. theorem OAI.LogConcaveSampling.AdjointRemoval.terminal_product_budget line 182
12. theorem OAI.LogConcaveSampling.AdjointRemoval.quantitative_branch_integral_bound line 224
13. lemma OAI.LogConcaveSampling.AdjointRemoval.lintegral_abs_list_sum_bound line 265
14. theorem OAI.LogConcaveSampling.AdjointRemoval.removal_sum_bound line 288