English
The continuous linear map f, together with a bound, yields a continuous linear map in the function space that agrees with f on the corresponding components.
Русский
Переход mkContinuous образует непрерывное линейное отображение, совпадающее с f на соответствующих компонентах.
LaTeX
$$f.mkContinuous C H$$
Lean4
/-- If a multilinear map in finitely many variables on normed spaces is continuous, then it
satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`, for some `C` which can be chosen to be
positive. -/
theorem exists_bound_of_continuous (f : MultilinearMap 𝕜 E G) (hf : Continuous f) :
∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
by
cases isEmpty_or_nonempty ι
· refine ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩
obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)
simp [univ_eq_empty, zero_le_one]
obtain ⟨ε : ℝ, ε0 : 0 < ε, hε : ∀ m : ∀ i, E i, ‖m - 0‖ < ε → ‖f m - f 0‖ < 1⟩ :=
NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one
simp only [sub_zero, f.map_zero] at hε
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
have : 0 < (‖c‖ / ε) ^ Fintype.card ι := pow_pos (div_pos (zero_lt_one.trans hc) ε0) _
refine ⟨_, this, ?_⟩
refine f.bound_of_shell_of_continuous hf (fun _ => ε0) (fun _ => hc) fun m hcm hm => ?_
refine (hε m ((pi_norm_lt_iff ε0).2 hm)).le.trans ?_
rw [← div_le_iff₀' this, one_div, ← inv_pow, inv_div, Fintype.card, ← prod_const]
gcongr
apply hcm
