OAI/Combinatorics/Progressions/Polynomial/AllocatedNestedDegreeInduction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile line 34
  2. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.degreeSourceCountConstants line 66
  3. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile line 69
  4. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeSourceProfile line 111
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBinLog_mono_netExponent line 137
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelMarkovPrecisionParameter_mono_netExponent line 149
  7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.mono_netExponent line 177
  8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeSourceProfile.mono_netExponent line 185
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelPreparationBinLog_mono_netExponent_calc line 203
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.positiveKernelMarkovPrecisionParameter_mono_netExponent_calc line 215
  11. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.mono_netExponent_calc line 243
  12. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.DegreeSourceProfile.mono_netExponent_calc line 251
  13. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.preparedCommonRadiusDegreeSourceProfile line 286
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.degreeGlobalizationAt_nested_suffix line 352
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.degreeGlobalizationAt_nested line 405
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.degreeGlobalizationAt_nested_of_recursive_inputs line 425