OAI/Combinatorics/Progressions/Estimates/PreparedRelativePositiveNativeRuleCanonical.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointCapExponent line 16
  2. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointCapExponent_two_le line 21
  3. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointCapExponent_primitive_le line 26
  4. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointCapExponent_density_le line 45
  5. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointForecastCap_le_work line 51
  6. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointMarginalCap_le_exp_work line 96
  7. def OAI.Erdos3.VectorPolynomial.candidateSourceRecursiveNextSeedExponent line 128
  8. theorem OAI.Erdos3.VectorPolynomial.candidateSourceRecursiveNextSeedExponent_ge_two line 132
  9. theorem OAI.Erdos3.VectorPolynomial.candidateSourceBackendPolynomial_le_next_seed line 137
  10. def OAI.Erdos3.VectorPolynomial.candidateSourceRecursiveUniformExponent line 154
  11. theorem OAI.Erdos3.VectorPolynomial.candidateSourceRecursiveUniformExponent_ge_two line 157
  12. theorem OAI.Erdos3.VectorPolynomial.candidateSourceRecursiveNextSeedExponent_le_uniform line 162
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.recursiveParameter_le_next_seed line 194
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.recursiveParameter_le_next_degree_seed line 213
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.recursiveParameter_le_next_degree_seed_of_uniform line 227
  16. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedFrontFitExponent line 254
  17. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedFrontFitExponent_ge_two line 259
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.familyParameter_pow_le_next_seed line 286
  19. theorem OAI.Erdos3.VectorPolynomial.exists_degreeGlobalizationAt_of_nested_source_data line 335
  20. theorem OAI.Erdos3.VectorPolynomial.exists_degreeGlobalizationAt_of_complete_nested_source_data line 441
  21. def OAI.Erdos3.VectorPolynomial.preparedRelativeNativeSourceExponent line 544
  22. def OAI.Erdos3.VectorPolynomial.preparedRelativePositiveExtra line 548
  23. def OAI.Erdos3.VectorPolynomial.preparedRelativePositiveSourceExponent line 552
  24. theorem OAI.Erdos3.VectorPolynomial.preparedRelativePositiveSourceExponent_bounds line 556
  25. def OAI.Erdos3.VectorPolynomial.preparedRelativePositiveEarlyExponent line 570
  26. theorem OAI.Erdos3.VectorPolynomial.preparedRelativePositiveEarlyExponent_two_le line 575
  27. def OAI.Erdos3.VectorPolynomial.preparedRelativePositiveInputExponent line 581
  28. theorem OAI.Erdos3.VectorPolynomial.preparedRelativePositiveInputExponent_spec line 585
  29. theorem OAI.Erdos3.VectorPolynomial.degreeGlobalizationAt_of_preparedRelativePositiveSource line 622
  30. theorem OAI.Erdos3.VectorPolynomial.degreeGlobalizationAt_of_preparedRelativePositiveSource_eq line 705
  31. theorem OAI.Erdos3.VectorPolynomial.degreeGlobalizationAt_of_preparedRelativePositiveSource_canonical line 792