OAI/RepresentationTheory/RestrictedTilting/WeightBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Binary weight bases and upper and lower unipotent degree bounds.

  1. def OAI.FiberFunctorProof.binaryExponentEquiv line 20
  2. def OAI.FiberFunctorProof.homogeneousMonomialBasis line 40
  3. def OAI.FiberFunctorProof.binaryBasis line 47
  4. lemma OAI.FiberFunctorProof.homogeneousMonomialBasis_apply line 51
  5. lemma OAI.FiberFunctorProof.binaryBasis_apply line 61
  6. lemma OAI.FiberFunctorProof.binaryBasis_finrank line 69
  7. lemma OAI.FiberFunctorProof.dualMatrix_diagonal line 74
  8. lemma OAI.FiberFunctorProof.linearChange_diagonal_X0 line 82
  9. lemma OAI.FiberFunctorProof.linearChange_diagonal_X1 line 88
  10. lemma OAI.FiberFunctorProof.costandard_basis_weight line 95
  11. lemma OAI.FiberFunctorProof.eigenvector_eq_zero_of_basis line 122
  12. lemma OAI.FiberFunctorProof.costandard_weight_bound line 152
  13. def OAI.FiberFunctorProof.HasWeightsBetween line 170
  14. lemma OAI.FiberFunctorProof.hasWeightsBetween_extension line 175
  15. lemma OAI.FiberFunctorProof.highest_unipotent_fixed line 196
  16. def OAI.FiberFunctorProof.lowerUnipotent line 229
  17. lemma OAI.FiberFunctorProof.lowerUnipotent_zero line 232
  18. lemma OAI.FiberFunctorProof.lowerUnipotent_add line 237
  19. lemma OAI.FiberFunctorProof.lowerUnipotent_inv line 245
  20. lemma OAI.FiberFunctorProof.lowerUnipotent_coordinate_mem_powerAlgebra line 251
  21. lemma OAI.FiberFunctorProof.polynomial_on_lowerUnipotent_mem_powerAlgebra line 260
  22. lemma OAI.FiberFunctorProof.rational_lowerUnipotent_expansion line 274
  23. lemma OAI.FiberFunctorProof.diagonal_lowerUnipotent line 288
  24. lemma OAI.FiberFunctorProof.lowerUnipotent_coefficient_weight line 298
  25. lemma OAI.FiberFunctorProof.lowerUnipotent_degree_bound line 334