OAI/Probability/LogConcave/Numerics/LogMeshLength.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.Quadrature.logMeshLength line 11
2. def OAI.LogConcaveSampling.Quadrature.logMeshCount line 12
3. def OAI.LogConcaveSampling.Quadrature.logMeshStep line 13
4. def OAI.LogConcaveSampling.Quadrature.logMeshNode line 14
5. lemma OAI.LogConcaveSampling.Quadrature.logMeshLength_pos line 16
6. lemma OAI.LogConcaveSampling.Quadrature.logMeshCount_pos line 20
7. lemma OAI.LogConcaveSampling.Quadrature.logMeshCount_bound line 27
8. lemma OAI.LogConcaveSampling.Quadrature.logMeshStep_pos line 31
9. lemma OAI.LogConcaveSampling.Quadrature.logMeshStep_le line 35
10. lemma OAI.LogConcaveSampling.Quadrature.logMeshStep_lower line 43
11. lemma OAI.LogConcaveSampling.Quadrature.logMeshNode_zero line 52
12. lemma OAI.LogConcaveSampling.Quadrature.logMeshNode_last line 55
13. lemma OAI.LogConcaveSampling.Quadrature.logMeshNode_sub line 63
14. lemma OAI.LogConcaveSampling.Quadrature.logMeshNode_strictMono line 71
15. lemma OAI.LogConcaveSampling.Quadrature.logMeshNode_mem line 85
16. lemma OAI.LogConcaveSampling.Quadrature.logMeshCell_upper line 92
17. lemma OAI.LogConcaveSampling.Quadrature.logMeshCell_lower line 103
18. lemma OAI.LogConcaveSampling.Quadrature.logMeshCell_upper_right line 137
19. lemma OAI.LogConcaveSampling.Quadrature.cell_singularity_cancel line 157
20. lemma OAI.LogConcaveSampling.Quadrature.cell_taylor_budget line 172