OAI/Combinatorics/Progressions/Estimates/ProductOrbitCongruence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.baseChange_mem_of_mapsTo line 12
  2. def OAI.Erdos3.realProductSingle line 25
  3. theorem OAI.Erdos3.realProductSingle_projection line 30
  4. theorem OAI.Erdos3.realProductSingle_projection_ne line 39
  5. theorem OAI.Erdos3.realProductSingle_mem_layer line 48
  6. theorem OAI.Erdos3.MultidegreeLieFiltration.realProductSingle_mem_layer line 79
  7. def OAI.Erdos3.MultidegreeLieFiltration.piRealOrbit line 95
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.piRealOrbit_eval line 106
  9. def OAI.Erdos3.NilpotentLieFiltration.piRealOrbit line 136
  10. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_eval line 148
  11. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_coefficient line 179
  12. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_project_log line 192
  13. theorem OAI.Erdos3.exists_real_firstProjection_lift line 210
  14. theorem OAI.Erdos3.exists_real_sparseProjection_lift line 216
  15. theorem OAI.Erdos3.real_four_sparse_lifts_vanish line 230
  16. theorem OAI.Erdos3.real_four_dependent_inputs_vanish line 274
  17. theorem OAI.Erdos3.NilpotentLieFiltration.piRealOrbit_eval_eq_of_log_eq line 302
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.pi_basis_eq_of_basis_eq line 320