English
Under DecidableEq on the index set, a refined bound for the variation of f on m1 and m2 is given, with explicit sum and product structure depending on the index set. This is a more precise version of the previous bound.
Русский
При наличии DecidableEq на индексном множестве приводится уточнённая граница вариации f на m1 и m2, с явной структурой суммы и произведений, зависящей от индексов.
LaTeX
$$$\|f(m_1) - f(m_2)\| \le \|f\| \cdot \sum_{i} \left(\prod_j \text{if } j=i \; \|m_{1j}-m_{2j}\| \text{ else } \max\{\|m_{1j}\|,\|m_{2j}\|\} \right)$$$
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 : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
‖f.mkContinuous C H‖ ≤ C :=
ContinuousMultilinearMap.opNorm_le_bound hC fun m => H m
