OAI/Combinatorics/Progressions/Estimates/AllocatedFrozenTaggedTwistStepDrop.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerSupported_polynomial_variation line 29
2. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.eval_sub_eval_of_component_dist line 62
3. theorem OAI.Erdos3.exists_native_twist_variation_slice_step_drop line 96
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.twist_variation line 241
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.frozen_twist_variation line 316
6. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_frozen_tagged_twist_step_drop line 397