OAI/Combinatorics/Progressions/Estimates/JoinedPairQuotientRefiltration.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorizationAtFast line 20
  2. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorization.exists_fastWitness line 35
  3. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorizationAtFast.graded_top_frequency line 43
  4. def OAI.Erdos3.NilpotentLieFiltration.joinedGradedPairFast line 63
  5. theorem OAI.Erdos3.NilpotentLieFiltration.joinedGradedPairFast_refiltered_mem line 68
  6. theorem OAI.Erdos3.NilpotentLieFiltration.joinedGradedPairFast_top_frequency line 82
  7. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairFastTop_le line 120
  8. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairFastTop_quotient_le line 134
  9. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairFastTop_quotient_kernel_eq_zero line 141
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_joinedPairFastTop_of_controlled_factorizations line 155
  11. theorem OAI.Erdos3.NilpotentLieFiltration.joinedGradedPairFast_graded line 216
  12. def OAI.Erdos3.NilpotentLieFiltration.joinedPairQuotientFast line 259
  13. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairQuotientFast_layer_eq line 268
  14. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairQuotientFast_graded line 283
  15. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairQuotientFast_layer_surjective line 295
  16. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairQuotientFast_top_le line 315
  17. theorem OAI.Erdos3.NilpotentLieFiltration.joinedPairQuotientFast_top_kernel_eq_zero line 328