OAI/Combinatorics/Progressions/Estimates/UnnormalizedCommonSymbolFactorization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_derivative_difference_inputs line 13
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_groupHom_coord line 51
  3. def OAI.Erdos3.NilpotentLieFiltration.nativeSymbolNormalize line 56
  4. theorem OAI.Erdos3.NilpotentLieFiltration.nativeSymbolNormalize_symbol line 62
  5. theorem OAI.Erdos3.NilpotentLieFiltration.nativeSymbolNormalize_constant line 73
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialHom_eq_of_symbol_eq line 83
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap_eq_of_symbol_eq line 96
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_eq_of_symbol_eq line 112
  9. theorem OAI.Erdos3.NilpotentLieFiltration.bounded_coefficient_derivative_point line 132
  10. theorem OAI.Erdos3.NilpotentLieFiltration.bounded_coefficient_derivative_family line 203
  11. theorem OAI.Erdos3.NilpotentLieFiltration.bounded_coefficient_difference_inputs line 260
  12. theorem OAI.Erdos3.NilpotentLieFiltration.common_coefficient_derivative_system line 318
  13. def OAI.Erdos3.NilpotentLieFiltration.BoundedInitialStateFactorization line 432
  14. def OAI.Erdos3.NilpotentLieFiltration.CommonInitialStateSpec line 447
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_from_common line 490
  16. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_initialState_bound line 551
  17. theorem OAI.Erdos3.NilpotentLieFiltration.BoundedInitialStateFactorization.mono line 596
  18. def OAI.Erdos3.NilpotentLieFiltration.FullInitialStateSpec line 607
  19. theorem OAI.Erdos3.NilpotentLieFiltration.exists_initialFormalState_from_common_family line 633
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_initialState_bound line 670
  21. def OAI.Erdos3.NilpotentLieFiltration.NormalizedTerminalFactorization line 711
  22. theorem OAI.Erdos3.NilpotentLieFiltration.NormalizedTerminalFactorization.mono line 721
  23. def OAI.Erdos3.NilpotentLieFiltration.NormalizedTerminalStateSpec line 732
  24. theorem OAI.Erdos3.NilpotentLieFiltration.exists_normalized_terminalState_bound line 750
  25. def OAI.Erdos3.NilpotentLieFiltration.CommonTerminalStateSpec line 813
  26. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_terminalState_bound line 840
  27. def OAI.Erdos3.NilpotentLieFiltration.TerminalCompositionSpec line 903
  28. theorem OAI.Erdos3.NilpotentLieFiltration.exists_terminalComposition_bound line 914
  29. def OAI.Erdos3.NilpotentLieFiltration.CommonFactorizationSpec line 1038
  30. theorem OAI.Erdos3.NilpotentLieFiltration.exists_commonFactorization_bound line 1066
  31. def OAI.Erdos3.NilpotentLieFiltration.CommonSymbolFactorizationSpec line 1127
  32. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_symbolFactorization_bound line 1156
  33. def OAI.Erdos3.NilpotentLieFiltration.UnnormalizedCommonSymbolFactorizationSpec line 1202
  34. theorem OAI.Erdos3.NilpotentLieFiltration.exists_unnormalized_common_symbolFactorization_bound line 1231