OAI/Combinatorics/Progressions/Estimates/UnconditionedArbitraryFixedPatchFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_relative_finite_returned_slice_normalization line 14
2. structure OAI.Erdos3.VectorPolynomial.AllocatedReturnedPatchSource line 125
3. def OAI.Erdos3.VectorPolynomial.AllocatedReturnedPatchSource.physical line 140
4. def OAI.Erdos3.VectorPolynomial.AllocatedReturnedPatchSource.chart line 143
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedReturnedPatchSource.chart_physical line 167
6. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedShearProblem line 179
7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedNormalizedShearProblem_of_returned_laws line 226
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedNormalizedShearProblem_of_returned_fiber_laws line 291
9. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFixedCenterNormalizedShearProblem line 380
10. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedZeroLayerNormalizedShearProblem line 480
11. def OAI.Erdos3.VectorPolynomial.AllocatedNormalizedCandidateConclusion line 558
12. theorem OAI.Erdos3.BooleanCubeKernel.exists_unconditioned_arbitrary_fixed_patch_family line 593