OAI/Probability/LogConcave/JetEstimates/ArrayRelabel.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.LogConcaveSampling.TensorEnergy.arrayRelabelline 13 - lemma
OAI.LogConcaveSampling.TensorEnergy.arrayTensor_relabelline 18 - lemma
OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.array_relabelline 28 - lemma
OAI.LogConcaveSampling.TensorEnergy.matrixArray_compline 38 - lemma
OAI.LogConcaveSampling.TensorEnergy.matrixComposition_splitline 51