OAI/Probability/LogConcave/Numerics/BasisDerivative.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_hasDerivAt line 15
2. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_deriv line 39
3. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_second_deriv line 44
4. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_joint_continuous line 51
5. def OAI.LogConcaveSampling.Quadrature.basisDerivative line 73
6. def OAI.LogConcaveSampling.Quadrature.derivativeInterpolation line 76
7. lemma OAI.LogConcaveSampling.Quadrature.basisDerivative_continuous line 79
8. lemma OAI.LogConcaveSampling.Quadrature.interpolation_hasDerivAt line 83
9. lemma OAI.LogConcaveSampling.Quadrature.derivativeInterpolation_chainTaylor line 89
10. lemma OAI.LogConcaveSampling.Quadrature.derivativeInterpolation_sub line 106
11. lemma OAI.LogConcaveSampling.Quadrature.derivative_cell_chain_error_eq line 112
12. lemma OAI.LogConcaveSampling.Quadrature.exists_basisDerivative_budget line 123
13. lemma OAI.LogConcaveSampling.RMSIntegral.smul_sq_bound line 149
14. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_cell_rms line 163
15. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_regularized_derivative_rms line 183
16. theorem OAI.LogConcaveSampling.Quadrature.derivative_cell_error_rms line 231
17. lemma OAI.LogConcaveSampling.Quadrature.regularized_intervalIntegrable line 306
18. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_chainTaylor_integral line 316
19. lemma OAI.LogConcaveSampling.Quadrature.zeroHermite_derivative_error_eq line 345
20. theorem OAI.LogConcaveSampling.Quadrature.zeroHermite_derivative_error_rms line 388