OAI/Combinatorics/Progressions/Estimates/ProjectedNativeCoefficient.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.adaptedTranslateLinear line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedTranslateLinear_coe line 25
  3. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolMap_adaptedTranslateLinear line 29
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolMap_translate line 34
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredPolynomialSymbolMap_extended line 59
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredPolynomialSymbolMap_polynomial line 67
  7. def OAI.Erdos3.NilpotentLieFiltration.PolynomialOrbit.translate line 97
  8. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval_translate line 102
  9. def OAI.Erdos3.RationalFilteredNilmanifold.integerOrbitPoint line 121
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.cyclicOrbitPoint_translate line 126
  11. def OAI.Erdos3.DegreeRankLieFiltration.nativeHorizontalCoefficientHom line 149
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.nativeHorizontalCoefficientHom_apply line 158
  13. theorem OAI.Erdos3.DegreeRankLieFiltration.nativeHorizontalCoefficientHom_tensor line 167
  14. theorem OAI.Erdos3.DegreeRankLieFiltration.nativeHorizontalCoefficientHom_translate line 180
  15. theorem OAI.Erdos3.DegreeRankLieFiltration.nativeHorizontalCoefficientHom_basis_independent line 194
  16. def OAI.Erdos3.NilpotentLieFiltration.realSquarePairHom line 227
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realSquarePairHom_component line 232
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realSquarePairHom_normalization line 249
  19. theorem OAI.Erdos3.exists_native_two_shift_normalization line 270
  20. theorem OAI.Erdos3.DegreeRankLieFiltration.projectedHorizontalSymbolCoefficient_native line 316