OAI/Combinatorics/Progressions/Probability/AllocatedExternalCandidateRetainedSliceLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedSite line 36
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedSite_val line 39
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.physical_retainedSite line 42
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedParameter_retainedSite line 45
  5. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw line 49
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_mean_parameter line 53
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_complexMean_parameter line 59
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_mean_physical line 66
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_complexMean_physical line 72
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_support line 79
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_retainedSite_pos line 91
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedLaw_original line 101
  13. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.siteLaw line 124
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.siteLaw_complexMean_physical line 129
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.siteLaw_support line 139
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.siteLaw_ambientPhysicalValue_score line 162
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.siteLaw_score line 174