OAI/Combinatorics/Progressions/Estimates/BoundedRealifiedSquareOrbit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.squareLayerConstraint line 16
  2. theorem OAI.Erdos3.NilpotentLieFiltration.squareLayer_eq_ker_constraint line 21
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareEquiv_mem_layer line 29
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareEquiv_symm_mem_layer line 46
  5. def OAI.Erdos3.NilpotentLieFiltration.realifiedSquareGroupEquiv line 66
  6. def OAI.Erdos3.NilpotentLieFiltration.realSquareFstHom line 77
  7. def OAI.Erdos3.NilpotentLieFiltration.realSquareSndHom line 81
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareGroupEquiv_fst line 85
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareGroupEquiv_snd line 90
  10. def OAI.Erdos3.NilpotentLieFiltration.realifiedSquareOrbit line 95
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareOrbit_eval line 103
  12. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareOrbit_fst line 114
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realifiedSquareOrbit_snd line 121
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareLattice_le_fst line 142
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareLattice_le_snd line 148
  16. def OAI.Erdos3.NilpotentLieFiltration.realSquareObservable line 154
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareObservable_mk line 160
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareObservable_norm_le line 170
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareObservable_top_invariant line 178
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_realSquare_observable_descent line 207
  21. theorem OAI.Erdos3.NilpotentLieFiltration.exists_lipschitz_realSquare_descent line 239
  22. theorem OAI.Erdos3.exists_bounded_normalized_square_orbit line 287
  23. theorem OAI.Erdos3.NilpotentLieFiltration.squareObservable_recovers_product line 333
  24. theorem OAI.Erdos3.exists_bounded_realified_square_orbit line 356
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareObservable_recovers_product line 391