English
If a multilinear map f on finitely many coordinates satisfies a pointwise bound on a shell around the origin, then the same bound holds globally.
Русский
Если многолинейное отображение f в конечном числе координат удовлетворяет по точкам ограничению на оболочке вокруг нуля, то такое же ограничение справедливо и глобально.
LaTeX
$$$\|f(m)\| \le C \prod i, \|m_i\| \quad \text{for all } m, \text{ given the shell condition}$$$
Lean4
/-- If a multilinear map in finitely many variables on normed spaces satisfies the inequality
`‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i` for some positive numbers `ε i`
and elements `c i : 𝕜`, `1 < ‖c i‖`, then it satisfies this inequality for all `m`. -/
theorem bound_of_shell (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜} (hε : ∀ i, 0 < ε i)
(hc : ∀ i, 1 < ‖c i‖)
(hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m : ∀ i, E i) :
‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
bound_of_shell_of_norm_map_coord_zero f (fun h ↦ by rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]) hε hc hf m
