OAI/Combinatorics/Progressions/Dynamics/AllocatedFixedPathAnchoredNativeComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_native_test_eq_eval line 63
2. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_native_rational_density_comparison line 115
3. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_recovered_native_rational_density_comparison line 282
4. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_recovered_physical_native_atom line 444
5. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_recovered_native_atom line 478
6. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_anchored_native_rational_density_comparison line 584