OAI/RepresentationTheory/FoulkesHowe/FlattenedForm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.flattenedSymmetricForm line 15

   Source documentation

   A form on symmetric powers, evaluated on products, is multilinear in all of the underlying vector factors.

   def flattenedSymmetricForm (T : SymmetricMultilinearForm a b V) :
       MultilinearMap ℂ (fun _ : Fin a × Fin b => V) ℂ :=
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm

2. theorem OAI.Problem346.flattenedSymmetricForm_apply line 21
3. theorem OAI.Problem346.flattenedSymmetricForm_inner_permute line 27

   Source documentation

   Independent permutations within the rows preserve the flattened form.

   theorem flattenedSymmetricForm_inner_permute
       (T : SymmetricMultilinearForm a b V)
       (σ : Fin a → Equiv.Perm (Fin b)) (v : Fin a × Fin b → V) :
       flattenedSymmetricForm T (fun p => v (p.1, σ p.1 p.2)) =
         flattenedSymmetricForm T v := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedSymmetricForm

4. theorem OAI.Problem346.flattenedSymmetricForm_outer_permute line 37

   Source documentation

   Symmetry of the original form permits permutation of the rows.

   theorem flattenedSymmetricForm_outer_permute
       (T : SymmetricMultilinearForm a b V)
       (hT : IsSymmetricMultilinearForm a b V T)
       (σ : Equiv.Perm (Fin a)) (v : Fin a × Fin b → V) :
       flattenedSymmetricForm T (fun p => v (σ p.1, p.2)) =
         flattenedSymmetricForm T v := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.IsSymmetricMultilinearForm, OAI.Problem346.flattenedSymmetricForm

5. abbrev OAI.Problem346.flattenedForm line 46

   Source documentation

   Compatibility API for the same flattened form, with inferred degrees.

   abbrev flattenedForm {a b : ℕ} {V : Type u} [AddCommGroup V] [Module ℂ V]
       (T : SymmetricMultilinearForm a b V) :
       MultilinearMap ℂ (fun _ : Fin a × Fin b => V) ℂ :=
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm

6. theorem OAI.Problem346.flattenedForm_apply line 52
7. theorem OAI.Problem346.flattenedForm_permute_factors line 56
8. theorem OAI.Problem346.flattenedForm_permute_slots line 63
9. theorem OAI.Problem346.flattenedForm_permute line 72

   Source documentation

   Simultaneous row and independent within-row permutation invariance.

   theorem flattenedForm_permute (a b : ℕ) (V : Type u)
       [AddCommGroup V] [Module ℂ V] (T : SymmetricMultilinearForm a b V)
       (hT : IsSymmetricMultilinearForm a b V T)
       (σ : Equiv.Perm (Fin a)) (τ : Fin a → Equiv.Perm (Fin b))
       (x : Fin a × Fin b → V) :
       flattenedForm T (fun p => x (σ p.1, τ p.1 p.2)) =
         flattenedForm T x :=
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.IsSymmetricMultilinearForm, OAI.Problem346.flattenedForm

10. theorem OAI.Problem346.flattenedForm_factor_perm line 83

    Source documentation

    Implicit-parameter factor symmetry used by the transfer sequences.

    theorem flattenedForm_factor_perm (T : SymmetricMultilinearForm a b V)
        (σ : Fin a → Equiv.Perm (Fin b)) (v : Fin a × Fin b → V) :
        flattenedForm T (fun p => v (p.1, σ p.1 p.2)) = flattenedForm T v :=
    …

    Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedForm

11. theorem OAI.Problem346.flattenedForm_row_perm line 89

    Source documentation

    Implicit-parameter row symmetry used by the transfer sequences.

    theorem flattenedForm_row_perm (T : SymmetricMultilinearForm a b V)
        (hT : IsSymmetricMultilinearForm a b V T) (σ : Equiv.Perm (Fin a))
        (v : Fin a × Fin b → V) :
        flattenedForm T (fun p => v (σ p.1, p.2)) = flattenedForm T v :=
    …

    Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.IsSymmetricMultilinearForm, OAI.Problem346.flattenedForm

12. theorem OAI.Problem346.flattenedForm_constant_rows line 95
13. theorem OAI.Problem346.flattenedForm_constant_columns line 100