English
A precise bound for the variation of f on two arguments m1 and m2 shows that the difference f(m1) − f(m2) is controlled by the operator norm of f and a sum of products involving the distances and norms of the arguments. This is a quantitative continuity estimate for multilinear maps.
Русский
Точная граница вариации отображения f на двух аргументах m1 и m2: разность f(m1) − f(m2) управляется нормой оператора f и суммой произведений, зависящих от расстояний и норм аргументов.
LaTeX
$$$\|f(m_1) - f(m_2)\| \le \|f\| \cdot \sum_i \left(\prod_j \|m_{1j} - m_{2j}\| \text{ или } \max\{\|m_{1j}\|,\|m_{2j}\|\} \right)$$$
Lean4
/-- The difference `f m₁ - f m₂` is controlled in terms of `‖f‖` and `‖m₁ - m₂‖`, less precise
version. For a more precise but less usable version, see `norm_image_sub_le'`.
The bound is `‖f m - f m'‖ ≤ ‖f‖ * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`. -/
theorem norm_image_sub_le (f : ContinuousMultilinearMap 𝕜 E G) (m₁ m₂ : ∀ i, E i) :
‖f m₁ - f m₂‖ ≤ ‖f‖ * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ :=
f.toMultilinearMap.norm_image_sub_le_of_bound (norm_nonneg _) f.le_opNorm _ _
