Coordinate expansion on the Fourier spatial carrier

Finite coordinate derivative estimates control multilinear derivatives with complex vector values.

theorem CKN.Leray.regularisedComplexMultilinear_norm_le_coordinateBound {n : ℕ} (T : Foundation.Parabolic.L2Vec3 [×n]→L[ℝ] ComplexVec3) (B : ℝ) (hB : 0 ≤ B) (hcoord : ∀ (w : Fin n → Fin 3), ‖T fun (k : Fin n) => regularisedSchwartzCoordinateDirection (w k)‖ ≤ B) : ‖T‖ ≤ ↑(Fintype.card (Fin n → Fin 3)) * B

A complex vector-valued multilinear map on the Fourier spatial carrier is controlled by its finitely many coordinate evaluations.