DiagonalCoefficient.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.diagonalPolynomial line 16
Source documentation
The one-variable polynomial obtained by restricting a multilinear form to an affine diagonal.
```
def diagonalPolynomial {a : ℕ} (T : MultilinearMap ℂ (fun _ : Fin a => E) ℂ)
    (x y : E) : Polynomial ℂ :=
…
```
lemma OAI.Problem346.diagonalPolynomial_eval line 21
lemma OAI.Problem346.diagonalPolynomial_coeff_one line 43

theorem OAI.Problem346.diagonal_linear_coefficient_zero line 57

Source documentation

If a multilinear form vanishes on an affine diagonal line, its linear diagonal coefficient vanishes. This statement does not require symmetry.

theorem diagonal_linear_coefficient_zero {a : ℕ}
    (T : MultilinearMap ℂ (fun _ : Fin a => E) ℂ) (x y : E)
    (h : ∀ c : ℂ, T (fun _ => x + c • y) = 0) :
    (∑ i : Fin a, T (Function.update (fun _ => x) i y)) = 0 := by
…

lemma OAI.Problem346.symmetric_update_eq line 67

Source documentation

Symmetry identifies the terms of the linear diagonal coefficient.

lemma symmetric_update_eq {a : ℕ}
    (T : MultilinearMap ℂ (fun _ : Fin a => E) ℂ)
    (hsym : ∀ (σ : Equiv.Perm (Fin a)) (v : Fin a → E),
      T (fun k => v (σ k)) = T v)
    (x y : E) (i j : Fin a) :
    T (Function.update (fun _ => x) j y) =
      T (Function.update (fun _ => x) i y) := by
…

theorem OAI.Problem346.symmetric_diagonal_mixed_zero line 90

Source documentation

Coefficient extraction for a symmetric multilinear form along an affine diagonal. This is the coefficient-of-c argument in the split binary form step.

theorem symmetric_diagonal_mixed_zero {a : ℕ}
    (T : MultilinearMap ℂ (fun _ : Fin a => E) ℂ)
    (hsym : ∀ (σ : Equiv.Perm (Fin a)) (v : Fin a → E),
      T (fun k => v (σ k)) = T v)
    (x y : E) (i : Fin a)
    (h : ∀ c : ℂ, T (fun _ => x + c • y) = 0) :
    T (Function.update (fun _ => x) i y) = 0 := by
…

theorem OAI.Problem346.symmetric_diagonal_cons_zero line 110

Source documentation

The same coefficient extraction with the distinguished slot placed first.

theorem symmetric_diagonal_cons_zero {r : ℕ}
    (T : MultilinearMap ℂ (fun _ : Fin (r + 1) => E) ℂ)
    (hsym : ∀ (σ : Equiv.Perm (Fin (r + 1))) (v : Fin (r + 1) → E),
      T (fun k => v (σ k)) = T v)
    (x y : E) (h : ∀ c : ℂ, T (fun _ => x + c • y) = 0) :
    T (Fin.cons y (fun _ : Fin r => x)) = 0 := by
…