English
For s ⊆ t and f: ι → 𝕜 with certain nonnegativity and closeness conditions, then d + (|s|/|t|) x^2 ≤ (∑_{i∈t} f_i^2)/|t|.
Русский
Для s ⊆ t и f: ι → 𝕜 при некоторых условиях неотрицательности и близости, имеем d + (|s|/|t|) x^2 ≤ (∑_{i∈t} f_i^2)/|t|.
LaTeX
$$If hst ⊆ t, f: ι → 𝕜, d ∈ 𝕜, hx ≥ 0, hs: x ≤ |(∑ i∈s f_i)/|s| − (∑ i∈t f_i)/|t||, and ht: d ≤ ((∑ i∈t f_i)/|t|)^2, then d + (|s|/|t|) x^2 ≤ (∑ i∈t f_i^2)/|t|.$$
Lean4
theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜) (hx : 0 ≤ x)
(hs : x ≤ |(∑ i ∈ s, f i) / #s - (∑ i ∈ t, f i) / #t|) (ht : d ≤ ((∑ i ∈ t, f i) / #t) ^ 2) :
d + #s / #t * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / #t :=
by
obtain hscard | hscard := ((#s).cast_nonneg : (0 : 𝕜) ≤ #s).eq_or_lt
· simpa [← hscard] using ht.trans sum_div_card_sq_le_sum_sq_div_card
have htcard : (0 : 𝕜) < #t := hscard.trans_le (Nat.cast_le.2 (card_le_card hst))
have h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / #s - (∑ i ∈ t, f i) / #t) ^ 2 := sq_le_sq.2 (by rwa [abs_of_nonneg hx])
have h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / #t)) / #s) ^ 2 :=
by
apply h₁.trans
rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
apply (add_le_add_right ht _).trans
rw [← mul_div_right_comm, le_div_iff₀ htcard, add_mul, div_mul_cancel₀ _ htcard.ne']
have h₃ := mul_sq_le_sum_sq hst (fun i => (f i - (∑ j ∈ t, f j) / #t)) h₂ hscard.ne'
apply (add_le_add_left h₃ _).trans
simp only [sub_div' htcard.ne', div_pow, ← sum_div, ← mul_div_right_comm _ (#t : 𝕜), ← add_div,
div_le_iff₀ (sq_pos_of_ne_zero htcard.ne'), sub_sq, sum_add_distrib, sum_const, sum_sub_distrib, mul_pow, ← sum_mul,
nsmul_eq_mul, two_mul]
ring_nf
rfl
