OAI/Probability/LogConcave/JetEstimates/ProperSplit.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.TensorEnergy.bound_norm line 14
2. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.norm_le line 22
3. lemma OAI.LogConcaveSampling.TensorEnergy.bound_iff_norm_le line 31
4. def OAI.LogConcaveSampling.TensorEnergy.ProperSplit line 53
5. instance OAI.LogConcaveSampling.TensorEnergy.(instance at line 55) line 55
6. def OAI.LogConcaveSampling.TensorEnergy.InSlots line 57
7. def OAI.LogConcaveSampling.TensorEnergy.OutSlots line 58
8. instance OAI.LogConcaveSampling.TensorEnergy.(instance at line 59) line 59
9. instance OAI.LogConcaveSampling.TensorEnergy.(instance at line 60) line 60
10. instance OAI.LogConcaveSampling.TensorEnergy.(instance at line 61) line 61
11. instance OAI.LogConcaveSampling.TensorEnergy.(instance at line 64) line 64
12. def OAI.LogConcaveSampling.TensorEnergy.splitEquiv line 68
13. def OAI.LogConcaveSampling.TensorEnergy.splitMatrix line 71
14. def OAI.LogConcaveSampling.TensorEnergy.splitEnvelope line 75
15. lemma OAI.LogConcaveSampling.TensorEnergy.splitEnvelope_nonneg line 78
16. lemma OAI.LogConcaveSampling.TensorEnergy.splitMatrix_norm_le line 81
17. def OAI.LogConcaveSampling.TensorEnergy.properOfEquiv line 88
18. def OAI.LogConcaveSampling.TensorEnergy.leftOfEquiv line 96
19. def OAI.LogConcaveSampling.TensorEnergy.rightOfEquiv line 106
20. lemma OAI.LogConcaveSampling.TensorEnergy.splitEquiv_ofEquiv line 117
21. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_envelope line 134
22. lemma OAI.LogConcaveSampling.TensorEnergy.splitEnvelope_le line 149
23. lemma OAI.LogConcaveSampling.TensorEnergy.measurable_splitEnvelope line 157