TransferDerivative.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.multilinearPolynomial_eq_slotPolynomial line 13
theorem OAI.Problem346.swap_pair_same_row line 25

theorem OAI.Problem346.flattenedForm_swap_row line 44

Source documentation

The flattened form is invariant under swapping two factors in a single row.

theorem flattenedForm_swap_row (a b : ℕ) (V : Type*)
    [AddCommGroup V] [Module ℂ V] (T : SymmetricMultilinearForm a b V)
    (i : Fin a) (j k : Fin b) (x : Fin a × Fin b → V) :
    flattenedForm T (x ∘ Equiv.swap (i,j) (i,k)) =
      flattenedForm T x := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.flattenedForm

theorem OAI.Problem346.flattened_derivative_eq_card_smul line 60

Source documentation

If the source label occurs only in one row, every occurrence gives the same coordinate-polynomial derivative term, by symmetry of factors in that row.

theorem flattened_derivative_eq_card_smul
    (a b : ℕ) (V K B : Type*) [AddCommGroup V] [Module ℂ V]
    [Fintype K] [DecidableEq B]
    (T : SymmetricMultilinearForm a b V) (e : K → V)
    (l : Fin a × Fin b → B) (src dst : B) (i : Fin a) (j : Fin b)
    (hj : l (i,j) = src)
    (hrow : ∀ p, l p = src → p.1 = i)
    (D : Derivation ℂ (MvPolynomial (B × K) ℂ) (MvPolynomial (B × K) ℂ))
    (hD : ∀ q k, D (MvPolynomial.X (q,k)) =
      if q = src then MvPolynomial.X (dst,k) else 0) :
    D (multilinearPolynomial (flattenedForm T) e l) =
      (Finset.univ.filter (fun p => l p = src)).card •
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.multilinearPolynomial, OAI.Problem346.flattenedForm

theorem OAI.Problem346.firstLabel_derivative line 91

Source documentation

The concrete one-step identity in the first transfer. The source is the t block; its remaining occurrences all lie in the distinguished row.

theorem firstLabel_derivative
    (r m k : ℕ) (hk : k < m) (V K : Type*)
    [AddCommGroup V] [Module ℂ V] [Fintype K]
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : K → V)
    (D : Derivation ℂ (MvPolynomial (FirstBlock m × K) ℂ)
      (MvPolynomial (FirstBlock m × K) ℂ))
    (hD : ∀ q j, D (MvPolynomial.X (q,j)) =
      if q = some none then MvPolynomial.X (some (some ⟨k,hk⟩),j) else 0) :
    D (multilinearPolynomial (flattenedForm T) e
        (firstLabel r m k)) =
      ((r+m-k : ℕ) : ℂ) •
        multilinearPolynomial (flattenedForm T) e
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.FirstBlock, OAI.Problem346.multilinearPolynomial, OAI.Problem346.flattenedForm, OAI.Problem346.firstLabel