OAI/Combinatorics/Progressions/Estimates/InitializedEarlyCanonicalSliceScales.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_early_allocated_canonical_slice_scales line 21
2. def OAI.Erdos3.VectorPolynomial.canonicalSublevelCutoffLip line 102
3. def OAI.Erdos3.VectorPolynomial.canonicalSublevelCutoff line 105
4. def OAI.Erdos3.VectorPolynomial.canonicalTransitionLip line 108
5. theorem OAI.Erdos3.VectorPolynomial.canonicalSublevelCutoff_spec line 111
6. theorem OAI.Erdos3.VectorPolynomial.canonicalTransitionLip_spec line 119
7. theorem OAI.Erdos3.VectorPolynomial.exists_initialized_early_canonical_slice_scales line 130
8. theorem OAI.Erdos3.VectorPolynomial.exists_primitive_early_canonical_slice_scales line 182