SecondEndpoints.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.SecondTransfer.initial_eval line 16
Source documentation
At the zero count vector, every row consists entirely of its independent vector.
```
theorem initial_eval {r b : ℕ} (T : SymmetricMultilinearForm (r+1) b V)
    (v : Block r → V) :
    flattenedSymmetricForm T (fun p => v (label (fun _ : Fin r => 0) p)) =
      T (fun i => symMonomial b V (fun _ => v (some i))) := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.SecondTransfer.Block, OAI.Problem346.flattenedSymmetricForm, OAI.Problem346.SecondTransfer.label, OAI.Problem346.symMonomial
theorem OAI.Problem346.SecondTransfer.terminal_eval line 24
Source documentation
At the terminal count vector, the first r factors in every moving row are the common vector. This is precisely the product form in the induction hypothesis.
```
theorem terminal_eval (r m : ℕ)
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (v : Block r → V) :
    flattenedSymmetricForm T (fun p => v (label (fun _ : Fin r => r) p)) =
      T (Fin.cons (symMonomial (r+m) V (fun _ => v (some 0)))
        (fun i => symPowMul r m (symMonomial r V (fun _ => v none))
          (symMonomial m V (fun _ => v (some i.succ))))) := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.SecondTransfer.Block, OAI.Problem346.flattenedSymmetricForm, OAI.Problem346.SecondTransfer.label, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul
theorem OAI.Problem346.SecondTransfer.terminal_eval_zero line 39
Source documentation
The known common-power vanishing implies the terminal labelled expression vanishes.
```
theorem terminal_eval_zero (r m : ℕ)
    (T : SymmetricMultilinearForm (r+1) (r+m) V)
    (h : ∀ x t : V, ∀ Q : Fin r → SymPow m V,
      T (Fin.cons (symMonomial (r+m) V (fun _ => t))
        (fun i => symPowMul r m (symMonomial r V (fun _ => x)) (Q i))) = 0)
    (v : Block r → V) :
    flattenedSymmetricForm T (fun p => v (label (fun _ : Fin r => r) p)) = 0 := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.SymPow, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul, OAI.Problem346.SecondTransfer.Block, OAI.Problem346.flattenedSymmetricForm, OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.terminal_polynomial_zero line 50

Source documentation

The terminal labelled polynomial is zero, before any degree-shift cancellation.

theorem terminal_polynomial_zero {κ : Type*} [Fintype κ] (r m : ℕ)
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : κ → V)
    (h : ∀ x t : V, ∀ Q : Fin r → SymPow m V,
      T (Fin.cons (symMonomial (r+m) V (fun _ => t))
        (fun i => symPowMul r m (symMonomial r V (fun _ => x)) (Q i))) = 0) :
    multilinearPolynomial (flattenedSymmetricForm T) e (label (fun _ : Fin r => r)) = 0 := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.SymPow, OAI.Problem346.symMonomial, OAI.Problem346.symPowMul, OAI.Problem346.multilinearPolynomial, OAI.Problem346.flattenedSymmetricForm, OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.independent_powers_zero_of_initial_polynomial_zero line 61
Source documentation
After cancelling all shifts, the initial polynomial identity evaluates to vanishing on independent pure powers in every slot.
```
theorem independent_powers_zero_of_initial_polynomial_zero
    {κ : Type*} [Fintype κ] {r b : ℕ}
    (T : SymmetricMultilinearForm (r+1) b V) (e : Module.Basis κ ℂ V)
    (h : multilinearPolynomial (flattenedSymmetricForm T) e
      (label (fun _ : Fin r => 0)) = 0) (v : Fin (r+1) → V) :
    T (fun i => symMonomial b V (fun _ => v i)) = 0 := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.multilinearPolynomial, OAI.Problem346.flattenedSymmetricForm, OAI.Problem346.SecondTransfer.label, OAI.Problem346.symMonomial