OAI/Probability/LogConcave/Numerics/ParametricFDeriv.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.CompactIntegral.parametric_hasFDerivAt line 16
2. theorem OAI.LogConcaveSampling.CompactIntegral.contDiff_parametric line 35
3. theorem OAI.LogConcaveSampling.CompactIntegral.smooth_parametric line 51