Operator Norm Bound by Coordinate Values

This bounds a continuous linear functional by its values on the standard basis.

For $n\in\mathbb N$ and a continuous linear map $A:(\operatorname{Fin}(n)\to\mathbb R)\to\mathbb R$, equipped with the supremum norm, one has

where $e_p=\operatorname{Pi.single}(p,1)$ is the $p$-th standard basis vector.

This coordinate estimate is used to control first derivatives by their partial derivatives.

Original Lean declaration header

Within namespace LevyStochCalc. Shown in its original module context. Proof omitted.

theorem norm_le_sum_abs_apply (A : (Fin n → ℝ) →L[ℝ] ℝ) :
    ‖A‖ ≤ ∑ p, |A (Pi.single p 1)|

Module navigation

Module: LevyStochCalc/Brownian/CoordDerivative.

Next: norm_le_sum_abs_apply₂.

Source excerpt, lines 144–145 · Frozen source 408915f.