OAI/Combinatorics/Progressions/Geometry/AllocatedReferenceSpatialRemeshing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.canonicalSpatialSiteDensity_lipschitz_ratio line 13
2. theorem OAI.Erdos3.canonicalSpatialSiteDensity_lipschitz_linear_width line 40
3. def OAI.Erdos3.VectorPolynomial.allocatedRefinedSpatialKernel line 122
4. def OAI.Erdos3.VectorPolynomial.allocatedRefinedReferenceReconstruction line 135
5. def OAI.Erdos3.VectorPolynomial.allocatedRefinedReferenceProfile line 141
6. def OAI.Erdos3.VectorPolynomial.allocatedRefinedReferenceSpatialMass line 151
7. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedReferenceSpatialMass_nonneg line 238
8. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedTupleReference_mesh_error line 256
9. theorem OAI.Erdos3.VectorPolynomial.allocatedRefinedSpatialKernel_remesh line 329