OAI/Combinatorics/Progressions/Estimates/ControlledDetectedTranslationBaseBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_eq_homogeneous_map line 21
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_homogeneous_coefficient line 28
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_homogeneous_eval line 35
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_mem_homogeneous_image line 42
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_coefficients_mem_homogeneous_image line 52
  6. theorem OAI.Erdos3.PolynomialTranslationLie.weightedSymbolRepresentative_mem_associatedGraded_image line 72
  7. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomialSymbolLift_value_mem_associatedGraded_image line 88
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_filteredMap_coefficient line 125
  9. theorem OAI.Erdos3.NilpotentLieFiltration.projected_realSymbolRepresentative_coefficient line 138
  10. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousProjected_scalar_coordinate line 153
  11. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneousProjected_scalar_identity line 179
  12. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseMap line 215
  13. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional line 224
  14. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_lie line 228
  15. theorem OAI.Erdos3.PolynomialTranslationLie.pairResidueTranslationProjection_coordinate_logHeight line 253
  16. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_basis_apply line 270
  17. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_basis_logHeight line 285
  18. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_basis_height line 303
  19. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_value_logHeight line 318
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_coordinate_top line 350
  21. theorem OAI.Erdos3.PolynomialTranslationLie.realifyTranslationBaseFunctional_eq_coord line 383
  22. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_pairOrbitSymbol line 403
  23. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_majorOrbitSymbol line 447
  24. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBase_slow_coefficients line 479
  25. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBase_exists_common_coefficient_grid line 498