OAI/Probability/LogConcave/JetEstimates/SplitIndex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.JetCalculus.gadj_scalar_at line 13
2. lemma OAI.LogConcaveSampling.TensorAtom.jetCard line 28
3. abbrev OAI.LogConcaveSampling.TensorAtom.SplitIndex line 36
4. lemma OAI.LogConcaveSampling.TensorAtom.splitIndex_nonempty line 39
5. def OAI.LogConcaveSampling.TensorAtom.splitAtom line 42
6. lemma OAI.LogConcaveSampling.TensorAtom.splitAtom_weight line 45
7. lemma OAI.LogConcaveSampling.TensorAtom.material_jetList line 48
8. lemma OAI.LogConcaveSampling.JetCalculus.dir_time line 109
9. lemma OAI.LogConcaveSampling.JetCalculus.mdir_time line 117
10. lemma OAI.LogConcaveSampling.JetCalculus.gadj_time_at line 123