OAI/RepresentationTheory/KazhdanLusztig/Invariance.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Genuine KL invariance, finite-parabolic transport and unrestricted finite interval models; the main theorem for two arbitrary Coxeter systems in four independent universes.

  1. theorem OAI.KLInvariance.rankDifference_subinterval_lt line 20
  2. theorem OAI.KLInvariance.rTilde_transport_all line 33
  3. theorem OAI.KLInvariance.BruhatGraph.actual_target_freeness line 77
  4. theorem OAI.KLInvariance.BruhatGraph.rTilde_eq_of_smaller_data line 95
  5. theorem OAI.KLInvariance.BruhatGraph.rTilde_freeness_of_below line 136
  6. theorem OAI.KLInvariance.BruhatGraph.rTilde_invariance_and_freeness line 190
  7. theorem OAI.KLInvariance.scaledKL_eq_scaledPolynomial line 224
  8. theorem OAI.KLInvariance.intervalIso_upper_rankDifference line 240
  9. theorem OAI.KLInvariance.scaledKL_transport line 247
  10. theorem OAI.KLInvariance.BruhatGraph.comparison_of_source02 line 269
  11. theorem OAI.KLInvariance.BruhatGraph.comparison_difference_le line 298
  12. theorem OAI.KLInvariance.BruhatGraph.bottom_eq_of_comparisons line 336
  13. theorem OAI.KLInvariance.BruhatGraph.rTilde_invariance_all_entries line 407
  14. theorem OAI.KLInvariance.BruhatGraph.scaledKL_eq_transported line 415
  15. theorem OAI.KLInvariance.BruhatGraph.klPolynomial_invariance_finite line 427
  16. structure OAI.KLInvariance.FiniteIntervalModel line 476
  17. theorem OAI.KLInvariance.exists_finiteIntervalModel line 484
  18. def OAI.KLInvariance.intervalEndpointCongr line 496
  19. def OAI.KLInvariance.FiniteIntervalModel.orderIso line 505
  20. theorem OAI.KLInvariance.FiniteIntervalModel.bruhat line 511
  21. theorem OAI.KLInvariance.FiniteIntervalModel.kl_eq line 517
  22. theorem OAI.KLInvariance.FiniteIntervalModel.rank_eq line 523
  23. theorem OAI.KLInvariance.combinatorial_invariance line 547

    Distinct definitions of this name: ComparatorChallenges/KLInvariance.lean:88 (same statement text; different proof or body). Qualify references as OAI.KLInvariance.combinatorial_invariance@path.