English
If an alternating map in finitely many variables on a normed space satisfies the inequality ‖f m‖ ≤ C ∏ ‖m i‖ on a shell, then it satisfies the same inequality for all m.
Русский
Если чередующее отображение в конечном числе переменных удовлетворяет неравенству на оболочке, то оно удовлетворяет тому же неравенству и для всех аргументов.
LaTeX
$$$\\forall m:\\, (\\forall i, 0<\\varepsilon_i) \\to (\\forall i, 1<\\|c_i\\|) \\to (\\forall m, (\\forall i, ε_i/\\|c_i\\| \\le \\|m_i\\|) \\to (\\forall i, \\|m_i\\|<ε_i) \\to \\|f m\\| ≤ C \\prod_i \\|m_i\\|) \\Rightarrow \\|f m\\| ≤ C \\prod_i \\|m_i\\|$$$
Lean4
/-- If an alternating map in finitely many variables on a normed space 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 : F [⋀^ι]→ₗ[𝕜] E) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜} (hε : ∀ i, 0 < ε i) (hc : ∀ i, 1 < ‖c i‖)
(hf : ∀ m : ι → F, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m : ι → F) :
‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
f.1.bound_of_shell hε hc hf m
