OAI/RepresentationTheory/FoulkesHowe/DiagonalPolarization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem346.continuous_symmetric_multilinear_eq_zero_of_diagonal line 11

   Source documentation

   A symmetric continuous multilinear form is determined by its diagonal.

   theorem continuous_symmetric_multilinear_eq_zero_of_diagonal
       {W : Type*} [NormedAddCommGroup W] [NormedSpace ℂ W] {n : ℕ}
       (T : ContinuousMultilinearMap ℂ (fun _ : Fin n => W) ℂ)
       (hsym : ∀ (σ : Equiv.Perm (Fin n)) (x : Fin n → W),
         T (fun i => x (σ i)) = T x)
       (hdiag : ∀ x : W, T (fun _ => x) = 0) : T = 0 := by
   …

2. theorem OAI.Problem346.symmetric_multilinear_eq_zero_of_diagonal line 27

   Source documentation

   Algebraic polarization, without a topology on the source vector space.

   theorem symmetric_multilinear_eq_zero_of_diagonal
       {W : Type*} [AddCommGroup W] [Module ℂ W] {n : ℕ}
       (T : MultilinearMap ℂ (fun _ : Fin n => W) ℂ)
       (hsym : ∀ (σ : Equiv.Perm (Fin n)) (x : Fin n → W),
         T (fun i => x (σ i)) = T x)
       (hdiag : ∀ x : W, T (fun _ => x) = 0) : T = 0 := by
   …