OAI/Probability/LogConcave/JetEstimates/MixedJetAdd.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_add line 21
2. lemma OAI.LogConcaveSampling.JetCalculus.dir_dir line 46
3. lemma OAI.LogConcaveSampling.JetCalculus.jet_perm line 62
4. lemma OAI.LogConcaveSampling.JetCalculus.dir_smul line 70
5. lemma OAI.LogConcaveSampling.JetCalculus.jet_smul line 75