OAI/RepresentationTheory/Saxl/StripReduction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Saxl.StripChain line 10
2. lemma OAI.Saxl.stripRemove_full_prefix line 15
3. theorem OAI.Saxl.stripChain_of_capacity line 22

   Source comment

   Sweeps remove any prescribed number within the first q-row capacity.

   theorem stripChain_of_capacity (q t : ℕ) (μ : YoungDiagram)
       (ht : t ≤ rowPrefix μ q) :
       ∃ k ≤ q, ∃ ν, ν.card + t = μ.card ∧ StripChain k ν μ := by
   …

   Mentions: OAI.Saxl.rowPrefix, OAI.Saxl.StripChain

4. lemma OAI.Saxl.rowPrefix_mean line 59
5. lemma OAI.Saxl.staircase_rowLen line 83
6. lemma OAI.Saxl.staircase_prefix_double line 92
7. lemma OAI.Saxl.strip_reduction_capacity line 105

   Source comment

   The exact capacity alternative used by the main induction.

   lemma strip_reduction_capacity (m : ℕ) (hm : 2 ≤ m) (μ : YoungDiagram)
       (hμ : μ.card = (staircase m).card) (hdom : ¬ Dominates (staircase m) μ)
       (hfirst : μ.rowLen 0 < m) : 5 ≤ m ∧ 2*m-1 ≤ rowPrefix μ 4 := by
   …

   Mentions: OAI.Saxl.staircase, OAI.Saxl.Dominates, OAI.Saxl.rowPrefix

8. theorem OAI.Saxl.strip_reduction line 139