OAI/Combinatorics/Progressions/Estimates/LowerStepSquare.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.squareLayer line 15
  2. theorem OAI.Erdos3.NilpotentLieFiltration.mem_squareLayer line 29
  3. theorem OAI.Erdos3.NilpotentLieFiltration.squareLayer_antitone line 33
  4. theorem OAI.Erdos3.NilpotentLieFiltration.squareLayer_lie_mem line 38
  5. def OAI.Erdos3.NilpotentLieFiltration.squareLieSubalgebra line 52
  6. theorem OAI.Erdos3.NilpotentLieFiltration.mem_squareLieSubalgebra line 56
  7. def OAI.Erdos3.NilpotentLieFiltration.squareFiltration line 61
  8. theorem OAI.Erdos3.NilpotentLieFiltration.mem_squareFiltration_layer line 78
  9. theorem OAI.Erdos3.NilpotentLieFiltration.mem_squareFiltration_top line 81
  10. def OAI.Erdos3.NilpotentLieFiltration.squareFst line 89
  11. def OAI.Erdos3.NilpotentLieFiltration.squareSnd line 92
  12. theorem OAI.Erdos3.NilpotentLieFiltration.squareFst_apply line 95
  13. theorem OAI.Erdos3.NilpotentLieFiltration.squareSnd_apply line 96
  14. theorem OAI.Erdos3.NilpotentLieFiltration.top_layer_central line 111
  15. theorem OAI.Erdos3.rationalLieInclusion_central line 117
  16. theorem OAI.Erdos3.scaled_basis_mem_bchSubgroup line 127
  17. theorem OAI.Erdos3.scaled_real_basis_mem_realification line 143
  18. theorem OAI.Erdos3.scaled_real_basis_central line 154
  19. theorem OAI.Erdos3.scaled_real_basis_coordinate_bound line 162
  20. theorem OAI.Erdos3.MultidegreeLieFiltration.omitted_weighted_top line 188
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTriple_top_group_relation line 194
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.additiveTriple_omitted_top_group_relation line 208
  23. def OAI.Erdos3.NilpotentLieFiltration.squareFstHom line 235
  24. def OAI.Erdos3.NilpotentLieFiltration.squareSndHom line 238
  25. theorem OAI.Erdos3.NilpotentLieFiltration.squareFstHom_coord line 241
  26. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndHom_coord line 244
  27. def OAI.Erdos3.NilpotentLieFiltration.squareLattice line 247
  28. theorem OAI.Erdos3.NilpotentLieFiltration.mem_squareLattice line 250
  29. theorem OAI.Erdos3.NilpotentLieFiltration.squareLattice_le_fst line 253
  30. theorem OAI.Erdos3.NilpotentLieFiltration.squareLattice_le_snd line 256
  31. theorem OAI.Erdos3.NilpotentLieFiltration.square_projections_joint_injective line 259
  32. theorem OAI.Erdos3.NilpotentLieFiltration.square_top_projections line 265
  33. theorem OAI.Erdos3.NilpotentLieFiltration.top_commutes line 271
  34. theorem OAI.Erdos3.cosetMap_smul line 280
  35. theorem OAI.Erdos3.NilpotentLieFiltration.realLayer_eq_span_basis line 302
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realLayer_le_span_scaled_basis line 311
  37. theorem OAI.Erdos3.MultidegreeLieFiltration.realAdditiveTripleProjection_mem line 339
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.realAdditiveTriple_top_group_relation line 353
  39. theorem OAI.Erdos3.MultidegreeLieFiltration.realAdditiveTriple_top_phase line 373
  40. theorem OAI.Erdos3.MultidegreeLieFiltration.realAdditiveTriple_omitted_top_group_relation line 387
  41. def OAI.Erdos3.NilpotentLieFiltration.squareObservable line 412
  42. theorem OAI.Erdos3.NilpotentLieFiltration.squareObservable_mk line 417
  43. theorem OAI.Erdos3.NilpotentLieFiltration.squareObservable_norm_le line 422
  44. theorem OAI.Erdos3.NilpotentLieFiltration.squareObservable_top_invariant line 429
  45. theorem OAI.Erdos3.NilpotentLieFiltration.exists_square_observable_descent line 450
  46. def OAI.Erdos3.NilpotentLieFiltration.squareReductionHom line 477
  47. theorem OAI.Erdos3.NilpotentLieFiltration.squareReductionHom_surjective line 481
  48. theorem OAI.Erdos3.NilpotentLieFiltration.squareReductionHom_ker line 484
  49. def OAI.Erdos3.NilpotentLieFiltration.reducedSquareOrbit line 487
  50. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareOrbit_eval line 491
  51. theorem OAI.Erdos3.NilpotentLieFiltration.exists_reduced_square_observable line 497