OAI/RepresentationTheory/RestrictedTilting/CharacterExpansions.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Character expansions on the diagonal torus and additive root group.

  1. lemma OAI.FiberFunctorProof.character_sum_eq_zero line 20
  2. def OAI.FiberFunctorProof.HasCharacterExpansions line 33
  3. lemma OAI.FiberFunctorProof.character_finsupp_eq_zero line 37
  4. lemma OAI.FiberFunctorProof.character_finsupp_ext line 45
  5. lemma OAI.FiberFunctorProof.character_coefficient_eigen line 56
  6. lemma OAI.FiberFunctorProof.eigenvector_lift line 82
  7. def OAI.FiberFunctorProof.characterFunctions line 106
  8. def OAI.FiberFunctorProof.characterAlgebra line 113
  9. lemma OAI.FiberFunctorProof.characterAlgebra_toSubmodule line 116
  10. lemma OAI.FiberFunctorProof.mem_characterAlgebra_iff line 122
  11. lemma OAI.FiberFunctorProof.character_mem_characterAlgebra line 137
  12. def OAI.FiberFunctorProof.characterEvaluation line 141
  13. lemma OAI.FiberFunctorProof.characterEvaluation_apply line 144
  14. lemma OAI.FiberFunctorProof.characterExpansions_of_coefficients line 149
  15. def OAI.FiberFunctorProof.diagonalTorus line 184
  16. def OAI.FiberFunctorProof.inverseUnitCharacter line 198
  17. lemma OAI.FiberFunctorProof.diagonal_coordinate_mem_characterAlgebra line 203
  18. lemma OAI.FiberFunctorProof.polynomial_on_torus_mem_characterAlgebra line 212
  19. lemma OAI.FiberFunctorProof.rational_torus_characterExpansions line 230
  20. lemma OAI.FiberFunctorProof.rational_weight_lift line 244
  21. def OAI.FiberFunctorProof.integerCharacter line 256
  22. lemma OAI.FiberFunctorProof.unit_power_functions_injective line 259
  23. lemma OAI.FiberFunctorProof.integerCharacter_injective line 272
  24. lemma OAI.FiberFunctorProof.vector_expansion_of_scalar_span line 295
  25. def OAI.FiberFunctorProof.integerFunctions line 332
  26. def OAI.FiberFunctorProof.integerAlgebra line 341
  27. lemma OAI.FiberFunctorProof.integerAlgebra_toSubmodule line 344
  28. lemma OAI.FiberFunctorProof.integerCharacter_mem_integerAlgebra line 349
  29. lemma OAI.FiberFunctorProof.diagonal_coordinate_mem_integerAlgebra line 353
  30. lemma OAI.FiberFunctorProof.polynomial_on_torus_mem_integerAlgebra line 367
  31. lemma OAI.FiberFunctorProof.rational_torus_integerExpansions line 383
  32. lemma OAI.FiberFunctorProof.function_sum_eq_zero line 405
  33. lemma OAI.FiberFunctorProof.function_finsupp_eq_zero line 417
  34. lemma OAI.FiberFunctorProof.function_finsupp_ext line 426
  35. lemma OAI.FiberFunctorProof.linearIndependent_powerFunctions line 439
  36. def OAI.FiberFunctorProof.powerFunctions line 459
  37. def OAI.FiberFunctorProof.powerAlgebra line 466
  38. lemma OAI.FiberFunctorProof.powerAlgebra_toSubmodule line 469
  39. lemma OAI.FiberFunctorProof.power_mem_powerAlgebra line 474
  40. lemma OAI.FiberFunctorProof.unipotent_coordinate_mem_powerAlgebra line 477
  41. lemma OAI.FiberFunctorProof.polynomial_on_unipotent_mem_powerAlgebra line 486
  42. lemma OAI.FiberFunctorProof.rational_unipotent_expansion line 500
  43. lemma OAI.FiberFunctorProof.diagonal_unipotent line 514
  44. lemma OAI.FiberFunctorProof.unipotent_coefficient_weight line 526