mul_sq_le_sum_sq — Mathlib

English

For s ⊆ t in a finite index set, and x with x^2 ≤ (sum over s of f)^2 / |s|^2 and |s| ≠ 0, then |s| · x^2 ≤ sum over t of f^2.

Русский

Для s ⊆ t и x с x^2 ≤ (∑_{i∈s} f_i / |s|)^2, |s| ≠ 0, тогда |s| x^2 ≤ ∑_{i∈t} f_i^2.

LaTeX

$$If s ⊆ t, f: ι → 𝕜, x ∈ 𝕜 with x^2 ≤ ((∑ i∈s f_i)/|s|)^2 and |s| ≠ 0, then (|s|)·x^2 ≤ ∑_{i∈t} f_i^2.$$

Lean4

theorem mul_sq_le_sum_sq (hst : s ⊆ t) (f : ι → 𝕜) (hs : x ^ 2 ≤ ((∑ i ∈ s, f i) / #s) ^ 2) (hs' : (#s : 𝕜) ≠ 0) :
    (#s : 𝕜) * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2 :=
  calc
    _ ≤ (#s : 𝕜) * ((∑ i ∈ s, f i ^ 2) / #s) := by
      gcongr
      exact hs.trans sum_div_card_sq_le_sum_sq_div_card
    _ = ∑ i ∈ s, f i ^ 2 := (mul_div_cancel₀ _ hs')
    _ ≤ ∑ i ∈ t, f i ^ 2 := by gcongr

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