FixedSlot.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.fixedSlotFlatten line 12
Source documentation
Flatten the remaining rows after fixing the first slot to a pure power.
```
def fixedSlotFlatten (T : SymmetricMultilinearForm (r+1) b V) (t : V) :
    MultilinearMap ℂ (fun _ : Fin r × Fin b => V) ℂ :=
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm
theorem OAI.Problem346.fixedSlotFlatten_apply line 16

theorem OAI.Problem346.fixedSlotFlatten_inner_permute line 23

Source documentation

Every row remains symmetric in its factors after fixing the first slot.

theorem fixedSlotFlatten_inner_permute
    (T : SymmetricMultilinearForm (r+1) b V) (t : V)
    (σ : Fin r → Equiv.Perm (Fin b)) (v : Fin r × Fin b → V) :
    fixedSlotFlatten T t (fun p => v (p.1, σ p.1 p.2)) = fixedSlotFlatten T t v :=
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.fixedSlotFlatten

theorem OAI.Problem346.fixedSlotFlatten_constant_rows line 30

Source documentation

Repeated vectors in the remaining rows are literal pure powers.

@[simp] theorem fixedSlotFlatten_constant_rows
    (T : SymmetricMultilinearForm (r+1) b V) (t : V) (v : Fin r → V) :
    fixedSlotFlatten T t (fun p => v p.1) =
      T (Fin.cons (symMonomial b V (fun _ => t))
        (fun i => symMonomial b V (fun _ => v i))) := rfl

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.fixedSlotFlatten, OAI.Problem346.symMonomial

theorem OAI.Problem346.fixedSlotFlatten_append line 37

Source documentation

Concatenating factors in every unfixed row computes graded multiplication.

theorem fixedSlotFlatten_append {m n : ℕ}
    (T : SymmetricMultilinearForm (r+1) (m+n) V) (t : V)
    (v : Fin r → Fin m → V) (w : Fin r → Fin n → V) :
    fixedSlotFlatten T t (fun p => Fin.append (v p.1) (w p.1) p.2) =
      T (Fin.cons (symMonomial (m+n) V (fun _ => t))
        (fun i => symPowMul m n (symMonomial m V (v i)) (symMonomial n V (w i)))) := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.fixedSlotFlatten, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul

theorem OAI.Problem346.fixedSlotFlatten_common_power line 46

Source documentation

The endpoint of the second shift chain has a common power factor in every row.

theorem fixedSlotFlatten_common_power {m : ℕ}
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (x t : V) (v : Fin r → V) :
    fixedSlotFlatten T t
      (fun p => Fin.append (fun _ : Fin r => x) (fun _ : Fin m => v p.1) p.2) =
      T (Fin.cons (symMonomial (r+m) V (fun _ => t))
        (fun i => symPowMul r m (symMonomial r V (fun _ => x))
          (symMonomial m V (fun _ => v i)))) := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.fixedSlotFlatten, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul

theorem OAI.Problem346.fixedSlotFlatten_swap_same_row line 56

Source documentation

Swapping two factor slots in the same unfixed row changes no value.

theorem fixedSlotFlatten_swap_same_row
    (T : SymmetricMultilinearForm (r+1) b V) (t : V)
    (p q : Fin r × Fin b) (hpq : p.1=q.1) (v : Fin r × Fin b → V) :
    fixedSlotFlatten T t (v ∘ Equiv.swap p q) = fixedSlotFlatten T t v :=
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.fixedSlotFlatten

theorem OAI.Problem346.fixedSlotFlatten_coeff_swap_same_row line 64

Source documentation

The fixed-slot coefficient array meets the row-swap hypothesis of shift recurrence.

theorem fixedSlotFlatten_coeff_swap_same_row {I : Type*}
    (T : SymmetricMultilinearForm (r+1) b V) (t : V) (e : I → V)
    (p q : Fin r × Fin b) (hpq : p.1=q.1) (k : Fin r × Fin b → I) :
    fixedSlotFlatten T t (e ∘ (k ∘ Equiv.swap p q)) = fixedSlotFlatten T t (e ∘ k) :=
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.fixedSlotFlatten