OAI/Probability/LogConcave/Sampling/FinsetSumSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.finset_sum_le_sum_of_eq line 15
2. lemma OAI.LogConcaveSampling.adjointCommutator_squared line 20
3. lemma OAI.LogConcaveSampling.tensorAdjoint_polySmooth line 59
4. lemma OAI.LogConcaveSampling.spatialEnergy_adjoint line 65
5. lemma OAI.LogConcaveSampling.spatialTensor_finRange_of_arrayBound line 115