OAI/Combinatorics/Progressions/Estimates/RealifiedDilationMultidegree.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.scaledPairLayer_eq_inf line 14
  2. theorem OAI.Erdos3.realPairEquiv_mem_scaledPairLayer line 20
  3. def OAI.Erdos3.realifiedScaledPairLayerEquiv line 32
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realPairEquiv_mem_dilationPairLayer line 57
  5. def OAI.Erdos3.NilpotentLieFiltration.realifiedDilationPairLayerEquiv line 63
  6. def OAI.Erdos3.NilpotentLieFiltration.realifiedDilationPairEquiv line 68
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedDilationPairEquiv_coe line 74
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedDilationPairEquiv_mem_layer line 79
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedDilationPairEquiv_symm_mem_layer line 92
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.strictUpperLayer_realification line 111
  11. theorem OAI.Erdos3.MultidegreeLieFiltration.realPairEquiv_mem_dilationPairLayer line 118
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedDilationPairEquiv_mem_multidegree line 127
  13. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedDilationPairEquiv_symm_mem_multidegree line 140