OAI/Probability/LogConcave/Numerics/ChainTaylor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.RMSIntegral.weighted_sum_sq_varying line 16
2. theorem OAI.LogConcaveSampling.RMSIntegral.weighted_time_seed line 53
3. lemma OAI.LogConcaveSampling.Quadrature.iteratedDerivWithin_chain line 89
4. lemma OAI.LogConcaveSampling.Quadrature.contDiffOn_chain line 100
5. def OAI.LogConcaveSampling.Quadrature.chainTaylor line 116
6. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_eq line 120
7. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_remainder line 129
8. theorem OAI.LogConcaveSampling.Quadrature.chainTaylor_remainder_rms line 162
9. lemma OAI.LogConcaveSampling.Quadrature.chainTaylor_scaled_eval line 215
10. lemma OAI.LogConcaveSampling.Quadrature.reproduces_cell_chainTaylor line 228
11. lemma OAI.LogConcaveSampling.Quadrature.interpolation_sub_unused line 236
12. lemma OAI.LogConcaveSampling.Quadrature.cell_chain_error_eq line 241
13. theorem OAI.LogConcaveSampling.Quadrature.cell_chain_error_rms line 265