English
Let f be a positive linear map from A1 to A2. Then there exists a bound C ≥ 0 such that for every a, ||f(a)|| ≤ C ||a||.
Русский
Пусть f — положительное линейное отображение от A1 в A2. Тогда существует граница C ≥ 0 такая, что для любого a выполняется ||f(a)|| ≤ C ||a||.
LaTeX
$$$$\exists C \in \mathbb{R}_{\ge 0}, \forall a, \|f(a)\| \le C \|a\|.$$$$
Lean4
/-- If `f` is a positive map, then it is bounded (and therefore continuous).
-/
theorem exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂) : ∃ C : ℝ≥0, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by
/- It suffices to only consider for positive `a`, by decomposing `a` into positive and negative
parts of the real and imaginary parts. -/
suffices h_nonneg : ∃ C : ℝ≥0, ∀ a, 0 ≤ a → ‖f a‖ ≤ C * ‖a‖
by
obtain ⟨C, hmain⟩ := h_nonneg
refine ⟨4 * C, fun x ↦ ?_⟩
obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x
conv_lhs => rw [hy]
simp only [map_sum, map_smul]
apply norm_sum_le _ _ |>.trans
simp only [norm_smul, norm_pow, norm_I, one_pow, one_mul]
apply Finset.sum_le_sum (g := fun _ ↦ C * ‖x‖) (fun i _ ↦ ?_) |>.trans <| by simp [mul_assoc]
apply hmain _ (hy_nonneg i) |>.trans
simp only
gcongr
exact hy_norm i
by_contra! hcontra
have (n : ℕ) : ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖ :=
by
obtain ⟨hx₁, hx₂⟩ := Classical.choose_spec (hcontra (2 ^ (2 * n)))
set x := Classical.choose (hcontra (2 ^ (2 * n)))
have hx := (eq_zero_or_norm_pos x).resolve_left (fun hx ↦ by simp_all)
refine ⟨‖x‖⁻¹ • x, smul_nonneg (by positivity) hx₁, ?_, ?_⟩
· simp [norm_smul, inv_mul_cancel₀ hx.ne']
· simpa [norm_smul] using (lt_inv_mul_iff₀' hx).mpr hx₂
choose x hx using this
simp only [forall_and] at hx
obtain ⟨hx_nonneg, hx_norm, hx⟩ := hx
have x_summable : Summable fun n : ℕ => (2 : ℝ) ^ (-(n : ℤ)) • x n :=
by
refine Summable.of_norm ?_
have : (2 : ℝ)⁻¹ < 1 := by norm_num
simp [norm_smul, hx_norm, ← inv_pow, this]
-- There is some `n` such that `‖f (∑' m, 2 ^ (-m) • x m)‖ < 2 ^ n`
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f (∑' (n : ℕ), (2 : ℝ) ^ (-(n : ℤ)) • x n)‖ < (2 : ℝ) ^ n :=
tendsto_pow_atTop_atTop_of_one_lt one_lt_two |>.eventually_gt_atTop _ |>.exists
apply hn.not_ge
trans ‖f ((2 : ℝ) ^ (-n : ℤ) • x n)‖
· have := hx n |>.le
rw [pow_mul', sq] at this
simpa [norm_smul] using (le_inv_mul_iff₀' (show 0 < (2 : ℝ) ^ n by positivity)).mpr this
· have (m : ℕ) : 0 ≤ ((2 : ℝ) ^ (-(m : ℤ)) • x m) := smul_nonneg (by positivity) (hx_nonneg m)
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg (this n)) ?_
gcongr
exact x_summable.le_tsum n fun m _ ↦ this m
