OAI/Combinatorics/Progressions/Estimates/AllocatedCanonicalUniformCoarseSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedSlicedSourceProjection.canonical_coarse_source line 106
2. theorem OAI.Erdos3.VectorPolynomial.canonical_rows_ambient_reinstance line 206
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_projection_data line 334
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_projected_coarse_source line 408
5. abbrev OAI.Erdos3.VectorPolynomial.canonicalCoverExponent line 641

   Distinct definitions of this name: OAI/Combinatorics/Progressions/Geometry/AllocatedCanonicalSpatialCoarseSource.lean:214 (same statement text; different proof or body). Qualify references as OAI.Erdos3.VectorPolynomial.canonicalCoverExponent@path.

6. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_uniform_projected_coarse_source line 754