OAI/Probability/LogConcave/Numerics/Basis.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.Quadrature.basis line 16
2. def OAI.LogConcaveSampling.Quadrature.interpolation line 19
3. def OAI.LogConcaveSampling.Quadrature.weight line 22
4. lemma OAI.LogConcaveSampling.Quadrature.basis_continuous line 24
5. lemma OAI.LogConcaveSampling.Quadrature.weight_integral line 27
6. lemma OAI.LogConcaveSampling.Quadrature.reproduces_scalar line 37
7. lemma OAI.LogConcaveSampling.Quadrature.reproduces_power line 44
8. lemma OAI.LogConcaveSampling.Quadrature.reproduces_vector line 51
9. lemma OAI.LogConcaveSampling.Quadrature.exists_basis_budget line 62
10. lemma OAI.LogConcaveSampling.RMSIntegral.norm_integral_sq line 89
11. lemma OAI.LogConcaveSampling.RMSIntegral.time_seed_sq line 104
12. lemma OAI.LogConcaveSampling.RMSIntegral.integrable_sq_of_uniform line 144
13. theorem OAI.LogConcaveSampling.RMSIntegral.time_seed_uniform line 158
14. lemma OAI.LogConcaveSampling.Quadrature.interpolation_continuous line 189
15. lemma OAI.LogConcaveSampling.Quadrature.weights_abs_bound line 192
16. def OAI.LogConcaveSampling.Quadrature.cellQuadrature line 207
17. lemma OAI.LogConcaveSampling.Quadrature.cellQuadrature_eq_integral line 210
18. theorem OAI.LogConcaveSampling.Quadrature.cellQuadrature_error_rms line 215
19. lemma OAI.LogConcaveSampling.RMSIntegral.norm_weighted_sum_sq line 270
20. theorem OAI.LogConcaveSampling.RMSIntegral.weighted_sum_sq line 282
21. lemma OAI.LogConcaveSampling.Quadrature.taylor_remainder_global line 324
22. lemma OAI.LogConcaveSampling.Quadrature.taylor_kernel_bound line 346
23. lemma OAI.LogConcaveSampling.Quadrature.taylor_scaled_eval line 368
24. lemma OAI.LogConcaveSampling.Quadrature.reproduces_cell_taylor line 382
25. lemma OAI.LogConcaveSampling.Quadrature.interpolation_sub line 390
26. lemma OAI.LogConcaveSampling.Quadrature.cell_error_eq line 395
27. theorem OAI.LogConcaveSampling.Quadrature.cell_error_rms line 419