OAI/Combinatorics/Progressions/Geometry/AllocatedSupportedBufferedPhysicalFactorization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedBufferedPhysicalChartRadius line 17
2. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedPhysicalChartRadius_pos line 21
3. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedPhysicalChartRadius_le_supported line 28
4. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedPhysicalChartRadius_le_original line 32
5. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedPhysicalChartRadius_budget line 36
6. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedPhysicalChartRadius_inv_le_exp line 53
7. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredSiteTerm_supported_buffered_factorization line 132
8. theorem OAI.Erdos3.VectorPolynomial.allocatedCoveredSiteTerm_supported_buffered_sum line 184
9. theorem OAI.Erdos3.BooleanCubeKernel.allocatedCoveredSiteTerm_supported_buffered_physical_factorization line 242