OAI/Probability/LogConcave/Numerics/Remainder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.Trapezoid.remainder line 21
2. lemma OAI.LogConcaveSampling.Trapezoid.contDiff_gradient line 24
3. lemma OAI.LogConcaveSampling.Trapezoid.hasFDerivAt_remainder line 28
4. lemma OAI.LogConcaveSampling.Trapezoid.derivative_remainder_littleO line 55
5. theorem OAI.LogConcaveSampling.Trapezoid.remainder_littleO line 80
6. lemma OAI.LogConcaveSampling.Trapezoid.remainder_bound line 89