OAI/Probability/LogConcave/Sampling/SpatialTensorContinuous.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.spatialTensor_continuous line 14
2. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_subsingleton line 33
3. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_zero line 42
4. lemma OAI.LogConcaveSampling.TensorEnergy.multilinearTensor_id_one line 47
5. lemma OAI.LogConcaveSampling.TensorEnergy.multilinearTensor_id_higher line 56
6. lemma OAI.LogConcaveSampling.TensorEnergy.multilinearTensor_id_bound line 63