OAI/Probability/LogConcave/JetEstimates/CrossMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.integral_mul_sq_le line 20
2. def OAI.LogConcaveSampling.Appell.crossMoment line 42
3. lemma OAI.LogConcaveSampling.Appell.sum_crossMoment line 47
4. theorem OAI.LogConcaveSampling.Appell.crossMoment_sq_bound line 73