OAI/Combinatorics/Progressions/Estimates/SymbolFastMembership.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedWeightedDilation_coe line 16
  2. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialSymbolDilation_repr line 21
  3. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilation line 32
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilation_tmul line 36
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilation_repr line 42
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilation_one line 55
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilation_mul line 61
  8. def OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilationHom line 68
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolDilationHom_coord line 72
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_dilation line 76
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_dilation line 88
  12. def OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorization line 117
  13. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorization.mono line 131
  14. def OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolCompositionSpec line 150
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_symbol_composition line 166
  16. theorem OAI.Erdos3.monomialScale_const_mul line 229
  17. theorem OAI.Erdos3.monomialScale_le_exp_mul line 236
  18. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_rescale line 262
  19. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorization.rescale line 285
  20. def OAI.Erdos3.NilpotentLieFiltration.SymbolFactorizationIn line 312
  21. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorization.exists_in line 320
  22. theorem OAI.Erdos3.NilpotentLieFiltration.SymbolFactorizationIn.mono line 333
  23. theorem OAI.Erdos3.monomialScale_div_const line 352
  24. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_dilation_ratio line 369
  25. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_dilation_inverse_scale line 380
  26. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_dilation_physical line 393
  27. def OAI.Erdos3.NilpotentLieFiltration.SymbolFastIn line 423
  28. theorem OAI.Erdos3.NilpotentLieFiltration.SymbolFactorizationIn.exists_fast_factors line 428