English
A less-precise bound states that the norm of f(m1) − f(m2) is bounded by a constant times the norm of the input difference, times a factor depending on the card of the index set and the norms of m1 and m2. This is a practical bound for estimates.
Русский
Менее строгая граница для нормы f(m1) − f(m2): норма ограничена константой, зависящей от размера индексов, норм m1 и m2 и расстояния между ними.
LaTeX
$$$\|f(m_1) - f(m_2)\| \le \|f\| \cdot |\iota| \cdot \max\{\|m_1\|,\|m_2\|\}^{|\iota|-1} \cdot \|m_1-m_2\|$$$
Lean4
/-- If a continuous multilinear map is constructed from a multilinear map via the constructor
`mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative. -/
theorem mkContinuous_norm_le' (f : MultilinearMap 𝕜 E G) {C : ℝ} (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
‖f.mkContinuous C H‖ ≤ max C 0 :=
ContinuousMultilinearMap.opNorm_le_bound (le_max_right _ _) fun m ↦
(H m).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity
