OAI/Probability/LogConcave/Numerics/OrdinaryDerivativeWeight.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.Quadrature.ordinaryDerivativeWeight line 16
2. lemma OAI.LogConcaveSampling.Quadrature.inv_intervalIntegrable line 19
3. lemma OAI.LogConcaveSampling.Quadrature.ordinaryDerivativeWeight_integrand_continuousOn line 25
4. lemma OAI.LogConcaveSampling.Quadrature.ordinaryDerivativeWeight_integral line 34
5. lemma OAI.LogConcaveSampling.Quadrature.derivativeInterpolation_joint_continuous line 56
6. lemma OAI.LogConcaveSampling.Quadrature.ordinaryDerivativeWeight_error_rms line 65
7. def OAI.LogConcaveSampling.terminalQuadratureWeight line 147
8. lemma OAI.LogConcaveSampling.probabilityNodes_zero line 153
9. lemma OAI.LogConcaveSampling.logMeshNode_pos line 156
10. lemma OAI.LogConcaveSampling.probabilityCellLength_le_h line 160
11. lemma OAI.LogConcaveSampling.logMeshFirst_lower line 167
12. lemma OAI.LogConcaveSampling.probabilityCellLength_ratio line 172
13. lemma OAI.LogConcaveSampling.Quadrature.regularized_intervalIntegrable_nonneg line 198
14. lemma OAI.LogConcaveSampling.Quadrature.regularized_integral_scale line 209
15. theorem OAI.LogConcaveSampling.terminalQuadrature_cell_rms line 233
16. lemma OAI.LogConcaveSampling.Quadrature.stronglyMeasurable_parametric_intervalIntegral line 325
17. lemma OAI.LogConcaveSampling.Quadrature.quadrature_error_sum line 333
18. theorem OAI.LogConcaveSampling.terminalQuadrature_analytic_rms line 354