OAI/Combinatorics/Progressions/Estimates/AllocatedCanonicalProjectedNativeSource.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedModelPhysicalExpansionIdentity.exists_uniform_canonical_normalized_native_model_of_positive_source line 88
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonical_finite_source_native line 304
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_constructed_native_source line 507
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_projected_native_source line 885