OAI/RepresentationTheory/FoulkesHowe/TransferEndpoints.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.firstVectors line 14

   Source documentation

   Assign vector values to the three kinds of blocks in the first transfer.

   def firstVectors {m : ℕ} (x t : V) (y : Fin m → V) : FirstBlock m → V
     | none => x
     | some none => t
     | some (some j) => y j
   
   omit [AddCommGroup V] [Module ℂ V] in

   Mentions: OAI.Problem346.FirstBlock

2. theorem OAI.Problem346.firstVectors_x line 20
3. theorem OAI.Problem346.firstVectors_t line 23
4. theorem OAI.Problem346.firstVectors_y line 26
5. theorem OAI.Problem346.firstLabel_initial_monomial line 29
6. theorem OAI.Problem346.firstLabel_other_monomial line 34
7. theorem OAI.Problem346.firstLabel_final_monomial line 47
8. theorem OAI.Problem346.firstLabel_initial_form line 75

   Source documentation

   Evaluation of the initial label configuration.

   theorem firstLabel_initial_form {r m : ℕ}
       (T : SymmetricMultilinearForm (r+1) (r+m) V) (x t : V) (y : Fin m → V) :
       flattenedForm T (fun p => firstVectors x t y (firstLabel r m 0 p)) =
         T (Fin.cons (symMonomial (r+m) V (fun _ => t))
           (fun _ => symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedForm, OAI.Problem346.firstVectors, OAI.Problem346.firstLabel, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul

9. theorem OAI.Problem346.firstLabel_final_form line 88

   Source documentation

   Evaluation of the terminal label configuration, with t^r times the common product.

   theorem firstLabel_final_form {r m : ℕ}
       (T : SymmetricMultilinearForm (r+1) (r+m) V) (x t : V) (y : Fin m → V) :
       flattenedForm T (fun p => firstVectors x t y (firstLabel r m m p)) =
         T (Fin.cons (symPowMul r m (symMonomial r V (fun _ => t)) (symMonomial m V y))
           (fun _ => symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) := by
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedForm, OAI.Problem346.firstVectors, OAI.Problem346.firstLabel, OAI.Problem346.symPowMul, OAI.Problem346.symMonomial

10. theorem OAI.Problem346.firstPolynomial_final_eq_zero line 101

    Source documentation

    The binary identity makes the terminal polynomial zero.

    theorem firstPolynomial_final_eq_zero {r m : ℕ}
        (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : κ → V)
        (h : ∀ (x t : V) (y : Fin m → V),
          T (Fin.cons (symPowMul r m (symMonomial r V (fun _ => t)) (symMonomial m V y))
            (fun _ => symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) = 0) :
        firstPolynomial T e m = 0 := by
    …

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

11. theorem OAI.Problem346.firstPolynomial_initial_vanishing line 119

    Source documentation

    A zero initial polynomial gives the freed-last-slot identity.

    theorem firstPolynomial_initial_vanishing {r m : ℕ}
        (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : Module.Basis κ ℂ V)
        (h : firstPolynomial T e 0 = 0) (x t : V) (y : Fin m → V) :
        T (Fin.cons (symMonomial (r+m) V (fun _ => t))
          (fun _ => symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) = 0 := by
    …

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