OAI/Combinatorics/Progressions/Probability/AllocatedExternalLocalSliceLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedParameter line 33
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.retainedParameter_parameter line 36
  3. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.SlicePoint line 41
  4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.sliceSite line 43
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.sliceSite_val line 46
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.physical_sliceSite line 49
  7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw line 52
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_mean line 56
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_complexMean line 62
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_mean_parameter line 68
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_complexMean_parameter line 74
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_mean_physical line 80
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_complexMean_physical line 85
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_support line 90
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.localLaw_sliceSite_pos line 102
  16. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.siteValue line 123
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.siteValue_sliceSite line 126
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.localLaw_score line 131