OAI/Combinatorics/Progressions/Estimates/SymbolAbsorptionBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_rational_closure line 14
  2. abbrev OAI.Erdos3.NilpotentLieFiltration.RealPolynomialSymbol line 78
  3. abbrev OAI.Erdos3.NilpotentLieFiltration.RealPolynomialSymbolGroup line 82
  4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_symbol_rational_closure line 87
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolBasis_bracket_support line 141
  6. def OAI.Erdos3.NilpotentLieFiltration.scaledRealPolynomialSymbolBasis line 155
  7. theorem OAI.Erdos3.NilpotentLieFiltration.scaledRealPolynomialSymbolBasis_repr line 160
  8. theorem OAI.Erdos3.NilpotentLieFiltration.scaledRealPolynomialSymbolBasis_structure line 167
  9. theorem OAI.Erdos3.NilpotentLieFiltration.scaledRealPolynomialSymbolBasis_bound_iff line 179
  10. theorem OAI.Erdos3.realDenominatorGrid_neg line 196
  11. def OAI.Erdos3.NilpotentLieFiltration.SymbolRationalGrid line 210
  12. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_inv line 217
  13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_rational_product_bound line 232
  14. def OAI.Erdos3.NilpotentLieFiltration.SymbolSlowBound line 286
  15. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_inv_iff line 294
  16. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_slow_product_bound line 301
  17. theorem OAI.Erdos3.NilpotentLieFiltration.symbolBasisIndex_monomial_ne_zero line 371
  18. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_log_norm line 378
  19. theorem OAI.Erdos3.NilpotentLieFiltration.sub_realGradeTruncation_mem line 405
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeTruncation_eq_iff line 412
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeTruncation_quotient line 420
  22. def OAI.Erdos3.NilpotentLieFiltration.truncateRealGrades line 428
  23. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealGrades_coord line 431
  24. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealGrades_quotient line 435
  25. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealGrades_mem_of_quotient_mem line 443
  26. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_mono line 474
  27. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_mono line 480
  28. def OAI.Erdos3.NilpotentLieFiltration.truncateRealSymbol line 485
  29. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealSymbol_coord line 490
  30. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealSymbol_slow line 495
  31. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealSymbol_rational line 502
  32. theorem OAI.Erdos3.NilpotentLieFiltration.truncateRealSymbol_quotient line 508
  33. def OAI.Erdos3.NilpotentLieFiltration.reindexSymbolBasisIndex line 530
  34. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolBasis_repr_reindex line 543
  35. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolBasis_repr_reindex line 552
  36. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_reindex_iff line 563
  37. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_reindex_iff line 576
  38. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_slow_mul_inv_bound line 609
  39. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_rational_inv_mul_bound line 634