SecondTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.SecondTransfer.polynomial_row_permute line 18

Source documentation

Polynomial encoding preserves the independent factor permutations of each row.

theorem polynomial_row_permute {κ : Type*} [Fintype κ] {r b : ℕ}
    (T : SymmetricMultilinearForm (r+1) b V) (e : κ → V)
    (l : Fin (r+1) × Fin b → Block r)
    (σ : Fin (r+1) → Equiv.Perm (Fin b)) :
    multilinearPolynomial (flattenedSymmetricForm T) e
        (fun p => l (p.1, σ p.1 p.2)) =
      multilinearPolynomial (flattenedSymmetricForm T) e l := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.SecondTransfer.Block, OAI.Problem346.multilinearPolynomial, OAI.Problem346.flattenedSymmetricForm

theorem OAI.Problem346.SecondTransfer.polynomial_step line 32

Source documentation

A single unfinished row can be recovered from its one-step progressed state.

theorem polynomial_step {κ : Type*} [Fintype κ] {r b : ℕ}
    (T : SymmetricMultilinearForm (r+1) b V) (e : κ → V)
    (hb : r * (r+1) ≤ b) (k : Fin r → ℕ) (hk : ∀ j, k j ≤ r)
    (i : Fin r) (hi : k i < r)
    (hnext : multilinearPolynomial (flattenedSymmetricForm T) e
      (label (Function.update k i (k i+1))) = 0) :
    multilinearPolynomial (flattenedSymmetricForm T) e (label k) = 0 := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.multilinearPolynomial, OAI.Problem346.flattenedSymmetricForm, OAI.Problem346.SecondTransfer.label

theorem OAI.Problem346.SecondTransfer.second_transfer line 58

Source documentation

The second differential transfer: remove the common degree-r power from all r moving arguments. Count-vector induction allows the shifts in any order.

theorem second_transfer [FiniteDimensional ℂ V] (r m : ℕ)
    (hb : r * (r+1) ≤ 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 : Fin (r+1) → V,
      T (fun i => symMonomial (r+m) V (fun _ => v i)) = 0 := by
…

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