OAI/Combinatorics/Progressions/Dynamics/TranslationMajorDetectedPotential.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.linearRestrictionArithmeticBudget_le_exp line 13
  2. theorem OAI.Erdos3.weightedPolynomialPotential_coeff line 76
  3. theorem OAI.Erdos3.weightedPolynomialPotential_height line 87
  4. theorem OAI.Erdos3.weightedPolynomialPotential_coefficient_grid line 103
  5. theorem OAI.Erdos3.exists_controlled_weighted_polynomial_primitive line 124
  6. def OAI.Erdos3.linearRestrictionLogPolynomial line 147
  7. theorem OAI.Erdos3.linearRestrictionLogPolynomial_eval line 153
  8. def OAI.Erdos3.projectedPotentialLogPolynomial line 163
  9. theorem OAI.Erdos3.potential_integration_height_le_exp line 168
  10. theorem OAI.Erdos3.linearRestrictionHeight_le_exp_logPolynomial line 189
  11. def OAI.Erdos3.projectedPotentialHeight line 200
  12. theorem OAI.Erdos3.projectedPotentialHeight_le_exp_logPolynomial line 204
  13. theorem OAI.Erdos3.exists_projectedPotential_height_budget line 229
  14. theorem OAI.Erdos3.PolynomialTranslationLie.exists_weighted_potential_on_base_image line 285
  15. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_polynomial_height_of_coordinates line 334
  16. theorem OAI.Erdos3.PolynomialTranslationLie.explicit_projected_weighted_potential line 350
  17. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_projection_polynomial_height line 409
  18. theorem OAI.MvPolynomial.IsWeightedHomogeneous.totalDegree_le_of_positive_weights line 440
  19. theorem OAI.Erdos3.PolynomialTranslationLie.exists_controlled_projected_potential_lifts line 456
  20. theorem OAI.Erdos3.PolynomialTranslationLie.exists_controlled_projected_potential line 524
  21. theorem OAI.Erdos3.PolynomialTranslationLie.exists_controlled_projected_potential_bounds line 590
  22. theorem OAI.Erdos3.PolynomialTranslationLie.exists_intrinsic_controlled_projected_potential_bounds line 649
  23. theorem OAI.Erdos3.PolynomialTranslationLie.exists_associatedGraded_controlled_potential line 726
  24. theorem OAI.Erdos3.PolynomialTranslationLie.exists_translationMajorDetectedPotential line 807