OAI/Geometry/CylinderCovering/Angular/SamplingArea.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularCovering.AngularSampling.nodeAlpha line 11
2. def OAI.TriangularCovering.AngularSampling.nodeBeta line 12
3. def OAI.TriangularCovering.AngularSampling.nodeSpeed line 13
4. def OAI.TriangularCovering.AngularSampling.sampleTerm line 15
5. lemma OAI.TriangularCovering.AngularSampling.node_bounds line 19
6. lemma OAI.TriangularCovering.AngularSampling.nodeAlpha_lipschitz line 38
7. lemma OAI.TriangularCovering.AngularSampling.nodeBeta_lipschitz line 47
8. lemma OAI.TriangularCovering.AngularSampling.density_lipschitz line 53
9. lemma OAI.TriangularCovering.AngularSampling.sample_term_remainder line 79
10. lemma OAI.TriangularCovering.AngularSampling.sample_integral_error line 98
11. lemma OAI.TriangularCovering.AngularSampling.partition_width_sum line 117
12. lemma OAI.TriangularCovering.AngularSampling.partition_density_sum line 125
13. theorem OAI.TriangularCovering.AngularSampling.sampled_sum_error line 132