OAI/Combinatorics/Progressions/Probability/AllocatedExternalCandidateAllSiteLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateWidths_eq line 22
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.law_eq_selectedJointFiniteLaw line 43
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.law_heq_of_parameters line 88
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.good_of_parameters line 100
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.bases_eq_prepared line 119
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.law_heq_prepared line 131
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.good_of_prepared line 137
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.measurable_good_of_prepared line 149
  9. def OAI.Erdos3.VectorPolynomial.allocatedExternalConditionalExcessExponent line 176
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalConditionalExcessExponent_spec line 179
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.site_nonempty line 205
  12. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.physicalBox line 208
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.physicalBox_val line 216
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.conditional_excess line 229
  15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.allSiteLaw line 338
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.allSiteLaw_retained line 342
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.allSiteLaw_of_mem line 346
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.allSiteLaw_restricted_residual_eq line 350
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.allSiteLaw_productive_residual_le_retained line 362
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.allSiteLaw_productive_residual_le line 377