OAI/Probability/LogConcave/Analysis/GaussianPairSumLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.gaussian_pair_sum_law line 14
2. lemma OAI.LogConcaveSampling.gaussian_pair_shift_law line 25
3. lemma OAI.LogConcaveSampling.law_add_gaussian line 33
4. lemma OAI.LogConcaveSampling.smoothing_add_gaussian line 52