OAI/Combinatorics/Progressions/Geometry/AllocatedCanonicalSpatialCoarseSource.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedSourceNumerics.canonical_spatial_size line 20
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedSourceNumerics.canonical_spatial_choices line 64
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSpatial_cutoff line 152
4. abbrev OAI.Erdos3.VectorPolynomial.canonicalCoverExponent line 214

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

5. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCanonicalSlice_spatial_projected_coarse_source line 314