OAI/RepresentationTheory/Saxl/RepeatedProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Saxl.weighted_perm_sum line 13
  2. theorem OAI.Saxl.pair_sum_rigidity line 20

    Source comment

    The strict square-moment equality used in the dominance projection. The labels may be real; the application uses actual nonnegative integer letters.
    theorem pair_sum_rigidity {X : Type uX} [Fintype X]
    (a t c : X → ℝ) (ω g h k : Equiv.Perm X)
    (hω : ∀ i, t (ω i) = t i) (hcomp : ∀ i, a i + a (ω i) = t i)
    (hg : ∀ i, t (g i) = t i) (hh : ∀ i, t (h i) = t i)
    (hc : ∀ i, c i = a (g i) + a (h i)) (hk : ∀ i, c i = t (k i)) : c = t := by
…
  3. def OAI.Saxl.wordOrbit line 60
  4. lemma OAI.Saxl.wordOrbit_perm line 63
  5. def OAI.Saxl.orbitProjection line 74
  6. def OAI.Saxl.pairSumMap line 86
  7. lemma OAI.Saxl.wordTensor_single line 91
  8. lemma OAI.Saxl.pairSumMap_single line 106
  9. lemma OAI.Saxl.altWord_inverse_sum line 119
  10. lemma OAI.Saxl.paired_relation_iff line 134
  11. lemma OAI.Saxl.paired_term_projection line 157
  12. theorem OAI.Saxl.repeated_alt_projection line 209