OAI/Combinatorics/Progressions/Estimates/ControlledPrescribedMarkedNativeFactorization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.filteredSymbolMapDenominator line 26
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredSymbolGroupMap_slow line 30
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredSymbolGroupMap_slow_exp line 60
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredSymbolGroupMap_grid line 82
  5. theorem OAI.Erdos3.NilpotentLieFiltration.filteredSymbolMapDenominator_pos line 102
  6. theorem OAI.Erdos3.NilpotentLieFiltration.filteredSymbolMapDenominator_le line 106
  7. theorem OAI.Erdos3.NilpotentLieFiltration.filteredSymbolMapDenominator_le_exp line 114
  8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_realFilteredSymbolGroupMap_grid line 128
  9. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_prescribed_fast_symbol_factorization line 171
  10. theorem OAI.Erdos3.NilpotentLieFiltration.realFilteredSymbolGroupMap_symbol line 433
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_refiltered_marked_symbol_factors line 442
  12. def OAI.Erdos3.NilpotentLieFiltration.fullMarkedNativeInput line 493
  13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_full_marked_native_factorizations line 496
  14. theorem OAI.Erdos3.NilpotentLieFiltration.exists_common_refiltered_terminal_discrepancies line 651
  15. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_prescribed_marked_native_factorizations line 768