English
For a multilinear map f, continuity implies the existence of a finite constant C with a global bound: ∥f m∥ ≤ C ∏ ∥m_i∥ for all m.
Русский
Для многообразной карты f непрерывность гарантирует существование конечной константы C, такой что ∥f(m)∥ ≤ C ∏ ∥m_i∥ для всех m.
LaTeX
$$$\exists C>0, \; \forall m, \; \|f(m)\| \le C \prod_i \|m_i\|$$$
Lean4
/-- If a multilinear map satisfies an inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`, then it is
continuous. -/
theorem continuous_of_bound (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : Continuous f :=
by
let D := max C 1
have D_pos : 0 ≤ D := le_trans zero_le_one (le_max_right _ _)
replace H (m) : ‖f m‖ ≤ D * ∏ i, ‖m i‖ := (H m).trans (mul_le_mul_of_nonneg_right (le_max_left _ _) <| by positivity)
refine continuous_iff_continuousAt.2 fun m => ?_
refine
continuousAt_of_locally_lipschitz zero_lt_one (D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1)) fun m' h' =>
?_
rw [dist_eq_norm, dist_eq_norm]
have : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1 := by simp [zero_le_one, norm_le_of_mem_closedBall (le_of_lt h')]
calc
‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
f.norm_image_sub_le_of_bound D_pos H m' m
_ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr
