OAI/RepresentationTheory/FoulkesHowe/Vanishing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.vanishing_induction_from_transfer_steps line 16

   Source documentation

   The induction on the number of slots, isolated from the two polynomial transfer arguments. The first argument packages the binary-pencil identity and the first transfer; the second is the common-power-removal transfer.

   theorem vanishing_induction_from_transfer_steps
       (firstTransfer : ∀ r m : ℕ, 0 < r → 0 < m → (r+1)*r ≤ r+m →
         ∀ T : SymmetricMultilinearForm (r+1) (r+m) V,
         IsSymmetricMultilinearForm (r+1) (r+m) V T →
         (∀ y : Fin (r+m) → V, T (fun _ => symMonomial (r+m) V y) = 0) →
         ∀ x t : V, ∀ y : Fin m → V,
           lowerProductForm r m T x t (fun _ => symMonomial m V y) = 0)
       (secondTransfer : ∀ r m : ℕ, 0 < r → 0 < m → (r+1)*r ≤ r+m →
         ∀ T : SymmetricMultilinearForm (r+1) (r+m) V,
         IsSymmetricMultilinearForm (r+1) (r+m) V T →
         (∀ x t : V, ∀ Q : Fin r → SymPow m V, lowerProductForm r m T x t Q = 0) →
         ∀ v : Fin (r+1) → V,
   …

   Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.IsSymmetricMultilinearForm, OAI.Problem346.symMonomial, OAI.Problem346.lowerProductForm, OAI.Problem346.SymPow