OAI/Probability/LogConcave/JetEstimates/MatrixArray.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.TensorEnergy.multilinearTensor_const_smul line 17
2. lemma OAI.LogConcaveSampling.probabilityVelocity_iterated_split line 26
3. theorem OAI.LogConcaveSampling.probabilityTransport_iterated_split line 45
4. def OAI.LogConcaveSampling.TensorEnergy.matrixArray line 115
5. lemma OAI.LogConcaveSampling.TensorEnergy.matrixArray_apply line 120
6. def OAI.LogConcaveSampling.TensorEnergy.jacobianSlots line 124
7. lemma OAI.LogConcaveSampling.TensorEnergy.jacobianSlots_symm_out line 135
8. lemma OAI.LogConcaveSampling.TensorEnergy.jacobianSlots_symm_last line 137
9. lemma OAI.LogConcaveSampling.TensorEnergy.jacobianSlots_symm_init line 139
10. lemma OAI.LogConcaveSampling.TensorEnergy.arrayTensor_jacobian line 142
11. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.jacobian line 160
12. lemma OAI.LogConcaveSampling.TensorEnergy.allSplit_jacobian_comp line 168