le_of_eq_sum_of_eq_sum_norm — Mathlib

English

Let f: ι → ℂ and s a finite set. If a = ∑_{i∈s} f(i) with a ≥ 0 and b = ∑_{i∈s} ‖f(i)‖, then a ≤ b. This is the scalar form of the triangle inequality.

Русский

Пусть f: ι → ℂ, s — конечное множество. Если a = ∑_{i∈s} f(i) и a ≥ 0, а b = ∑_{i∈s} |f(i)|, то a ≤ b. Это числовая форма неравенства треугольника.

LaTeX

$$$ 0 \\le a \\;\\land\\; a = \\sum_{i \\in s} f(i) \\;\\land\\; b = \\sum_{i \\in s} |f(i)| \\Rightarrow a \\le b $$$

Lean4

theorem le_of_eq_sum_of_eq_sum_norm {ι : Type*} {a b : ℝ} (f : ι → ℂ) (s : Finset ι) (ha₀ : 0 ≤ a)
    (ha : a = ∑ i ∈ s, f i) (hb : b = ∑ i ∈ s, (‖f i‖ : ℂ)) : a ≤ b := by norm_cast at hb;
  rw [← Complex.norm_of_nonneg ha₀, ha, hb]; exact norm_sum_le s f

Похожие утверждения