OAI/Combinatorics/Progressions/Geometry/AllocatedSupportedSlicedUniformPhysicalSource.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedDeck_density_constant line 59
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedCoveredFactor_mean line 72
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedLongProfile_constant line 93
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedMaskedCoveredFactor_mean line 160
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedMaskedProfile_chart_mean line 251
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSliced_referenceCell_pos line 275
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedProductProfile_chart_error line 353
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedProductProfile_error line 393
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedProductProfile_combined_error line 424
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_sliced_ideal_model line 550
  11. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_sliced_source_model line 717
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_sliced_uniform_source_model line 864
  13. theorem OAI.Erdos3.VectorPolynomial.oneCubeAllRows line 1012
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_supported_sliced_uniform_physical_source line 1074