OAI/Combinatorics/Progressions/Estimates/TranslationLogSlowNormalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.scaleMvPolynomialAxes_eq_eval₂Hom line 14
2. theorem OAI.Erdos3.scaleMvPolynomialAxes_eval_div line 24
3. theorem OAI.Erdos3.realPolynomialMass_scaleMvPolynomialAxes line 32
4. theorem OAI.Erdos3.realPolynomialMass_scaleMvPolynomialAxes_of_div line 46
5. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_totalDegree_le line 65
6. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_slow_normalized_mass line 80