OAI/Probability/LogConcave/JetEstimates/AssignmentsFinset.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.JetCalculus.assignments_toFinset line 25
2. lemma OAI.LogConcaveSampling.JetCalculus.assignments_nodup line 35
3. lemma OAI.LogConcaveSampling.JetCalculus.assignments_sum line 45
4. theorem OAI.LogConcaveSampling.JetCalculus.jet_prod_sum line 52
5. lemma OAI.LogConcaveSampling.JetCalculus.smooth_right_jet line 61
6. theorem OAI.LogConcaveSampling.JetCalculus.mixedJet_prod_sum line 67
7. lemma OAI.LogConcaveSampling.Appell.slotPolynomial_fiber line 103
8. lemma OAI.LogConcaveSampling.Appell.filter_nil_iff_card_fiber line 121
9. lemma OAI.LogConcaveSampling.Appell.mixedJet_reduced_fibers line 138
10. lemma OAI.LogConcaveSampling.Appell.mixedJet_reduced_pow line 164
11. lemma OAI.LogConcaveSampling.Appell.mixedCumulant_eq_range line 179
12. lemma OAI.LogConcaveSampling.Appell.mixedJet_log_crossMGF line 199
13. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_fst line 228
14. lemma OAI.LogConcaveSampling.JetCalculus.mixedJet_snd line 233
15. lemma OAI.LogConcaveSampling.Appell.log_crossMGF line 247
16. theorem OAI.LogConcaveSampling.Appell.mixedJet_log_laplace line 261
17. theorem OAI.LogConcaveSampling.Appell.actual_cumulant_energy line 288