OAI/Combinatorics/Progressions/Linear/BoundedAdaptedBasis.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.span_inter_eq_of_spanning_family line 17
  2. theorem OAI.Erdos3.exists_sorted_flag_basis_from_spanning_set line 30
  3. def OAI.Erdos3.basisTail line 83
  4. theorem OAI.Erdos3.basisTail_antitone line 93
  5. theorem OAI.Erdos3.basisTail_zero line 96
  6. theorem OAI.Erdos3.basisTail_terminal line 101
  7. theorem OAI.Erdos3.basisTail_eq_span line 109
  8. theorem OAI.Erdos3.basis_mem_tail line 121
  9. theorem OAI.Erdos3.mem_basisTail_succ_iff line 126
  10. theorem OAI.Erdos3.sub_coordinate_mem_tail line 138
  11. def OAI.Erdos3.IsCentralLieBasis line 152
  12. theorem OAI.Erdos3.IsCentralLieBasis.lie_mem_tail_succ line 160
  13. def OAI.Erdos3.IsCentralLieBasis.tailIdeal line 173
  14. theorem OAI.Erdos3.IsCentralLieBasis.coordinate_lie_eq_zero line 179
  15. theorem OAI.Erdos3.centralLieBasis_of_sorted_filtration line 184
  16. theorem OAI.Erdos3.finite_flag_weight_le line 217
  17. theorem OAI.Erdos3.centralLieBasis_of_finite_flag line 227
  18. theorem OAI.Erdos3.NilpotentLieFiltration.layer_eq_span_of_weighted_flag line 269
  19. theorem OAI.Erdos3.NilpotentLieFiltration.exists_sorted_adapted_basis line 295
  20. theorem OAI.Erdos3.NilpotentLieFiltration.exists_central_basis line 304
  21. def OAI.Erdos3.weightCut line 319
  22. theorem OAI.Erdos3.weightCut_le line 323
  23. theorem OAI.Erdos3.weight_gt_iff_cut_le line 328
  24. theorem OAI.Erdos3.span_weight_gt_eq_basisTail line 354
  25. def OAI.Erdos3.realBasisTail line 375
  26. theorem OAI.Erdos3.realBasisTail_antitone line 385
  27. theorem OAI.Erdos3.realBasisTail_zero line 388
  28. theorem OAI.Erdos3.realBasisTail_terminal line 393
  29. theorem OAI.Erdos3.realBasisTail_eq_span line 401
  30. theorem OAI.Erdos3.real_basis_mem_tail line 413
  31. theorem OAI.Erdos3.mem_realBasisTail_succ_iff line 418
  32. theorem OAI.Erdos3.real_sub_coordinate_mem_tail line 430
  33. def OAI.Erdos3.IsRealCentralLieBasis line 444
  34. theorem OAI.Erdos3.IsRealCentralLieBasis.lie_mem_tail_succ line 452
  35. def OAI.Erdos3.IsRealCentralLieBasis.tailIdeal line 465
  36. theorem OAI.Erdos3.IsRealCentralLieBasis.coordinate_lie_eq_zero line 471
  37. theorem OAI.Erdos3.IsCentralLieBasis.real_baseChange line 485
  38. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_sorted_adapted_basis line 510