OAI/Combinatorics/Progressions/Linear/WeightedTranslationBasisHeight.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialTranslationLie.constantDirection line 14
  2. def OAI.Erdos3.PolynomialTranslationLie.topProjection line 16
  3. theorem OAI.Erdos3.PolynomialTranslationLie.topProjection_base line 29
  4. theorem OAI.Erdos3.PolynomialTranslationLie.topProjection_polynomial line 34
  5. theorem OAI.Erdos3.PolynomialTranslationLie.topProjection_mem_top line 39
  6. theorem OAI.Erdos3.PolynomialTranslationLie.topProjection_pure line 46
  7. theorem OAI.Erdos3.PolynomialTranslationLie.pure_constant_zero_of_top_frequency line 53
  8. theorem OAI.Erdos3.PolynomialTranslationLie.raw_lie_mem line 65
  9. def OAI.Erdos3.PolynomialTranslationLie.relationSpace line 73
  10. theorem OAI.Erdos3.PolynomialTranslationLie.mem_relationSpace line 77
  11. def OAI.Erdos3.PolynomialTranslationLie.potentialRelationOfTopFrequency line 81
  12. theorem OAI.Erdos3.PolynomialTranslationLie.mem_potentialRelationOfTopFrequency line 96
  13. theorem OAI.Erdos3.PolynomialTranslationLie.exists_weighted_potential_of_top_frequency line 106
  14. theorem OAI.Erdos3.PolynomialTranslationLie.exponential_closure_potential_of_top_frequency line 123
  15. def OAI.Erdos3.PolynomialTranslationLie.weightedCoordinatesEquiv line 156
  16. abbrev OAI.Erdos3.PolynomialTranslationLie.WeightedBasisIndex line 168
  17. def OAI.Erdos3.PolynomialTranslationLie.weightedBasis line 171
  18. def OAI.Erdos3.PolynomialTranslationLie.weightedBasisGrade line 177
  19. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_repr_inl line 180
  20. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_repr_inr line 186
  21. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasisGrade_inl line 192
  22. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasisGrade_inr line 196
  23. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_projection_base line 200
  24. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_projection_coeff line 207
  25. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_top_projection_polynomial line 215
  26. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_top_projection_val line 245
  27. theorem OAI.Erdos3.PolynomialTranslationLie.weightedFiltration_layer_eq_span line 254
  28. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_top_projection_eq line 295
  29. theorem OAI.Erdos3.PolynomialTranslationLie.topProjection_mem_map_of_basisGraded line 301
  30. theorem OAI.Erdos3.PolynomialTranslationLie.topProjection_mem_of_basisGraded line 311
  31. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_projection_isWeightedHomogeneous line 324
  32. theorem OAI.Erdos3.PolynomialTranslationLie.exists_homogeneous_coordinate_lifts line 339
  33. theorem OAI.Erdos3.PolynomialTranslationLie.exists_ambient_homogeneous_coordinate_lifts line 370
  34. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasisGrade_pos line 390
  35. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasisGrade_le line 397
  36. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasisIndex_finite line 403
  37. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_base_height line 423
  38. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_polynomial_height line 430
  39. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_height_iff line 445