VanishingFirst.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.lowerProductForm_diagonal_zero line 17
Source documentation
Diagonal vanishing gives the diagonal vanishing of the lower-arity form. This combines binary splitting, coefficient extraction, and the first transfer.
```
theorem lowerProductForm_diagonal_zero (r m : ℕ) (hr : 0 < r)
    (T : SymmetricMultilinearForm (r+1) (r+m) V)
    (hT : IsSymmetricMultilinearForm (r+1) (r+m) V T)
    (hdiag : ∀ 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 := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.IsSymmetricMultilinearForm, OAI.Problem346.symMonomial, OAI.Problem346.lowerProductForm

theorem OAI.Problem346.vanishing_on_products_of_second_transfer line 27

Source documentation

With the first transfer and pure-power detection established, the common-power removal transfer is the sole remaining input to the vanishing induction.

theorem vanishing_on_products_of_second_transfer
    (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,
        T (fun i => symMonomial (r+m) V (fun _ => v i)) = 0) :
    ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → a*(a-1) ≤ b →
      ∀ T : SymmetricMultilinearForm a b V,
      IsSymmetricMultilinearForm a b V T →
      (∀ y : Fin b → V, T (fun _ => symMonomial b V y) = 0) → T = 0 := by
…

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