The norm of a multilinear map on an orthonormal basis

A continuous multilinear map M on finite-dimensional inner product spaces is determined by its values on tuples of vectors of orthonormal bases b j, and its operator norm is controlled by them: ‖M‖ ≤ ∑_r ‖M (fun j => b j (r j))‖, the sum running over all tuples r of basis indices (ContinuousMultilinearMap.opNorm_le_sum_norm_apply_orthonormalBasis). For a second derivative, this bounds the norm of the Hessian by the sum of the absolute values of its matrix entries. The linear case, ‖L‖ ≤ ∑ i, ‖L (b i)‖, is ContinuousLinearMap.opNorm_le_sum_norm_apply_orthonormalBasis; for a first derivative it bounds the norm of the gradient by the sum of the absolute values of the partial derivatives. Its square form ‖L‖² ≤ (card ι) ∑ i, ‖L (b i)‖² (ContinuousLinearMap.opNorm_sq_le_card_mul_sum_norm_apply_sq_orthonormalBasis) bounds the norm of a matrix by its columns in square mean.

Conversely, the entries H ![b i, b j] of a bilinear map on an orthonormal basis are bounded by the operator norm (ContinuousMultilinearMap.norm_apply_orthonormalBasis_le). For a bilinear map H on a space with an orthonormal basis indexed by ι, an entry bound ‖H ![b i, b j]‖ ≤ B gives ‖H‖ ≤ (card ι)² B (ContinuousMultilinearMap.opNorm_le_card_sq_mul_of_norm_apply_le). A Hölder family of bilinear maps has Hölder entries with the same constant (HolderOnWith.apply_orthonormalBasis), and conversely a family whose entries are Hölder with constant C is Hölder with constant (card ι)² C (HolderOnWith.of_apply_orthonormalBasis). These are the bounds relating a Hessian to its matrix entries.

theorem ContinuousLinearMap.opNorm_le_sum_norm_apply_orthonormalBasis {𝕜 : Type u_1} {E : Type u_2} {G : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (L : E →L[𝕜] G) (b : OrthonormalBasis ι 𝕜 E) : ‖L‖ ≤ ∑ i : ι, ‖L (b i)‖

The operator norm of a continuous linear map on an inner product space is at most the sum of the norms of its values on the vectors of an orthonormal basis.

theorem ContinuousLinearMap.opNorm_sq_le_card_mul_sum_norm_apply_sq_orthonormalBasis {𝕜 : Type u_1} {E : Type u_2} {G : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (L : E →L[𝕜] G) (b : OrthonormalBasis ι 𝕜 E) : ‖L‖ ^ 2 ≤ ↑(Fintype.card ι) * ∑ i : ι, ‖L (b i)‖ ^ 2

The squared operator norm of a continuous linear map on an inner product space is at most the number of vectors of an orthonormal basis times the sum of the squared norms of its values on them.

theorem ContinuousMultilinearMap.opNorm_le_sum_norm_apply_orthonormalBasis {𝕜 : Type u_1} {G : Type u_2} {κ : Type u_3} {E : κ → Type u_4} {ι : κ → Type u_5} [RCLike 𝕜] [(j : κ) → NormedAddCommGroup (E j)] [(j : κ) → InnerProductSpace 𝕜 (E j)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [(j : κ) → Fintype (ι j)] [Fintype κ] (M : ContinuousMultilinearMap 𝕜 E G) (b : (j : κ) → OrthonormalBasis (ι j) 𝕜 (E j)) : ‖M‖ ≤ ∑ r : (j : κ) → ι j, ‖M fun (j : κ) => (b j) (r j)‖

The operator norm of a continuous multilinear map on inner product spaces is at most the sum of the norms of its values on tuples of vectors of orthonormal bases, one for each argument.

theorem ContinuousMultilinearMap.norm_apply_orthonormalBasis_le {𝕜 : Type u_1} {E : Type u_2} {G : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (H : E [×2]→L[𝕜] G) (b : OrthonormalBasis ι 𝕜 E) (i j : ι) : ‖H ![b i, b j]‖ ≤ ‖H‖

An entry H ![b i, b j] of a bilinear map on an orthonormal basis b has norm at most the operator norm.

theorem ContinuousMultilinearMap.opNorm_le_card_sq_mul_of_norm_apply_le {𝕜 : Type u_1} {E : Type u_2} {G : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (H : E [×2]→L[𝕜] G) (b : OrthonormalBasis ι 𝕜 E) {B : ℝ} (hB : ∀ (i j : ι), ‖H ![b i, b j]‖ ≤ B) : ‖H‖ ≤ ↑(Fintype.card ι) ^ 2 * B

A bilinear map whose entries H ![b i, b j] on an orthonormal basis b are bounded by B has operator norm at most (card ι)² B.

theorem HolderOnWith.apply_orthonormalBasis {𝕜 : Type u_1} {E : Type u_2} {G : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {X : Type u_5} [PseudoEMetricSpace X] {H : X → E [×2]→L[𝕜] G} {C r : NNReal} {s : Set X} (h : HolderOnWith C r H s) (b : OrthonormalBasis ι 𝕜 E) (i j : ι) : HolderOnWith C r (fun (x : X) => (H x) ![b i, b j]) s

A family of bilinear maps which is Hölder on a set has entries H x ![b i, b j], on an orthonormal basis b, which are Hölder there with the same constant.

theorem HolderOnWith.of_apply_orthonormalBasis {𝕜 : Type u_1} {E : Type u_2} {G : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] {X : Type u_5} [PseudoMetricSpace X] {H : X → E [×2]→L[𝕜] G} {C r : NNReal} {s : Set X} (b : OrthonormalBasis ι 𝕜 E) (h : ∀ (i j : ι), HolderOnWith C r (fun (x : X) => (H x) ![b i, b j]) s) : HolderOnWith (↑(Fintype.card ι) ^ 2 * C) r H s

A family of bilinear maps whose entries H x ![b i, b j], on an orthonormal basis b indexed by ι, are Hölder on a set with constant C is Hölder there with constant (card ι)² C. This is the converse of HolderOnWith.apply_orthonormalBasis.