MultilinearPolynomial.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.multilinearPolynomial line 16
Source documentation
The scalar polynomial obtained by feeding a multilinear form vector variables, with block i specifying which vector variable occurs in its ith argument.
```
def multilinearPolynomial (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : κ → V) (block : ι → β) : MvPolynomial (β × κ) ℂ := by
…
```

theorem OAI.Problem346.eval_multilinearPolynomial line 24

Source documentation

Evaluation of the multilinear polynomial on arbitrary coordinate assignments.

theorem eval_multilinearPolynomial
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : κ → V) (block : ι → β) (z : β × κ → ℂ) :
    MvPolynomial.eval z (multilinearPolynomial L e block) =
      L (fun i => ∑ k, z (block i, k) • e k) := by
…

Mentions: OAI.Problem346.multilinearPolynomial

theorem OAI.Problem346.eval_multilinearPolynomial_basis line 40

Source documentation

With basis coordinates, evaluation is literal evaluation on the chosen vector blocks.

theorem eval_multilinearPolynomial_basis
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : Module.Basis κ ℂ V) (block : ι → β) (v : β → V) :
    MvPolynomial.eval (fun z : β × κ => e.repr (v z.1) z.2)
      (multilinearPolynomial L e block) = L (fun i => v (block i)) := by
…

Mentions: OAI.Problem346.multilinearPolynomial

theorem OAI.Problem346.multilinearPolynomial_eq_zero line 49

Source documentation

Pointwise vanishing on vector blocks implies the corresponding polynomial identity.

theorem multilinearPolynomial_eq_zero
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : κ → V) (block : ι → β)
    (h : ∀ v : β → V, L (fun i => v (block i)) = 0) :
    multilinearPolynomial L e block = 0 := by
…

Mentions: OAI.Problem346.multilinearPolynomial

theorem OAI.Problem346.multilinearPolynomial_eq_zero_iff line 60

Source documentation

Conversely, a polynomial identity gives the vector-valued identity by basis evaluation.

theorem multilinearPolynomial_eq_zero_iff
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : Module.Basis κ ℂ V) (block : ι → β) :
    multilinearPolynomial L e block = 0 ↔
      ∀ v : β → V, L (fun i => v (block i)) = 0 := by
…

Mentions: OAI.Problem346.multilinearPolynomial

theorem OAI.Problem346.multilinearPolynomial_perm line 71

Source documentation

Reindexing the labels by a symmetry of the multilinear form leaves its polynomial unchanged.

theorem multilinearPolynomial_perm
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : κ → V) (block : ι → β) (σ : Equiv.Perm ι)
    (hσ : ∀ x : ι → V, L (fun i => x (σ i)) = L x) :
    multilinearPolynomial L e (fun i => block (σ i)) =
      multilinearPolynomial L e block := by
…

Mentions: OAI.Problem346.multilinearPolynomial

theorem OAI.Problem346.multilinearPolynomial_update_eq line 83

Source documentation

Equal labels make replacing either of two symmetric slots give the same polynomial.

theorem multilinearPolynomial_update_eq [DecidableEq ι]
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : κ → V) (block : ι → β) (i j : ι) (dst : β)
    (hij : block i = block j)
    (hsym : ∀ x : ι → V, L (fun k => x (Equiv.swap i j k)) = L x) :
    multilinearPolynomial L e (Function.update block i dst) =
      multilinearPolynomial L e (Function.update block j dst) := by
…

Mentions: OAI.Problem346.multilinearPolynomial

theorem OAI.Problem346.multilinearPolynomial_sum_updates line 111

Source documentation

The derivative's sum over interchangeable source slots is a scalar multiple of one term.

theorem multilinearPolynomial_sum_updates [DecidableEq ι]
    (L : MultilinearMap ℂ (fun _ : ι => V) ℂ)
    (e : κ → V) (block : ι → β) (s : Finset ι) (j : ι) (dst : β)
    (hlabel : ∀ i ∈ s, block i = block j)
    (hsym : ∀ i ∈ s, ∀ x : ι → V,
      L (fun k => x (Equiv.swap i j k)) = L x) :
    (∑ i ∈ s, multilinearPolynomial L e (Function.update block i dst)) =
      (s.card : ℂ) • multilinearPolynomial L e (Function.update block j dst) := by
…

Mentions: OAI.Problem346.multilinearPolynomial