OAI/Probability/LogConcave/Numerics/CompositeAngle.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.Quadrature.compositeAngle line 15
2. lemma OAI.LogConcaveSampling.Quadrature.compositeAngle_mem line 19
3. def OAI.LogConcaveSampling.Quadrature.compositeWeight line 24
4. lemma OAI.LogConcaveSampling.Quadrature.compositeWeight_budget line 27
5. lemma OAI.LogConcaveSampling.Quadrature.compositeWeight_sum line 43
6. lemma OAI.LogConcaveSampling.Quadrature.composite_error_rms line 50
7. lemma OAI.LogConcaveSampling.Quadrature.compositeIntegral_sum line 81
8. lemma OAI.LogConcaveSampling.Quadrature.compositeQuadrature_defect line 114
9. def OAI.LogConcaveSampling.Quadrature.derivativeWeight line 144
10. def OAI.LogConcaveSampling.Quadrature.derivativeStencil line 147
11. lemma OAI.LogConcaveSampling.Quadrature.derivative_reproduces_scalar line 150
12. lemma OAI.LogConcaveSampling.Quadrature.derivative_reproduces_power line 158
13. lemma OAI.LogConcaveSampling.Quadrature.derivative_weights_norm line 171
14. lemma OAI.LogConcaveSampling.Quadrature.derivative_reproduces_vector line 176
15. theorem OAI.LogConcaveSampling.Quadrature.derivative_stencil_error_rms line 207
16. theorem OAI.LogConcaveSampling.Quadrature.endpoint_quotient_rms line 258
17. theorem OAI.LogConcaveSampling.Quadrature.endpoint_integral_rms line 283