OAI/Combinatorics/Progressions/Polynomial/AllocatedZeroLayerDegreeScalarConclusion.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.PolynomialPatch.ExternalObservableRegularity line 25
  2. theorem OAI.Erdos3.PolynomialPatch.externalObservableRegularity_of_niltest_complexity line 37
  3. theorem OAI.Erdos3.PolynomialPatch.ExternalObservableRegularity.mono line 47
  4. theorem OAI.Erdos3.PolynomialPatch.shearObservable_memberNets line 61
  5. theorem OAI.Erdos3.exists_polynomialPatch_external_observable_budget line 74
  6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeGlobalizationAt line 122
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.degreeGlobalizationAt_zero line 148
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeGlobalizationAt.mono_output line 154
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeGlobalizationAt.mono_input line 196
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeGlobalizationAt.mono_netExponent line 222
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_shearDegreeGlobalization line 284
  12. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedShearObservableExponent line 323
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedNormalizedShearObservableExponent_ge_two line 326
  14. def OAI.Erdos3.VectorPolynomial.allocatedNormalizedCandidateBudget line 330
  15. theorem OAI.Erdos3.VectorPolynomial.childCost_le_allocatedNormalizedCandidateBudget line 334
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_normalizedShearDegreeConclusion line 377
  17. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.normalizedShearDegreeConclusion line 412
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedNormalizedCandidateConclusion.degreeGlobalization line 435
  19. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedZeroLayer_degree_scalar_conclusion line 496