Prove2Me

Finite-Sum Euclidean Triangle Inequality

Proved
FunctionalInequalities.KLS.BKL.sqrt_sum_sq_sum_le_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the finite-sum Minkowski inequality for coordinatewise square sums.

Let ι\iota and κ\kappa be finite types, let ss be a finite subset of κ\kappa, and let f:κ→ι→Rf:\kappa\to\iota\to\mathbb{R}. Then

∑i(∑q∈sf(q,i))2≤∑q∈s∑if(q,i)2.\sqrt{\sum_i\left(\sum_{q\in s}f(q,i)\right)^2} \le \sum_{q\in s}\sqrt{\sum_i f(q,i)^2}.

This general finite-dimensional inequality is reused to separate mask contributions in cumulant-energy estimates.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL. Shown in its original module context. Proof omitted.

theorem sqrt_sum_sq_sum_le {ι κ : Type*} [Fintype ι] (s : Finset κ) (f : κ → ι → ℝ) :
    Real.sqrt (∑ i, (∑ q ∈ s, f q i) ^ 2) ≤ ∑ q ∈ s, Real.sqrt (∑ i, f q i ^ 2)

Module navigation

Module: KLS/BKL/CumulantEnergy/Basic.

Previous: sum_selected_eq · Next: sum_sq_pairTerm_ofFn_le.

Source excerpt, lines 237–238 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnergy_Basic
Formal statement

theorem FunctionalInequalities.KLS.BKL.sqrt_sum_sq_sum_le_readable {ι κ : Type*} [Fintype ι] (s : Finset κ) (f : κ → ι → ℝ) :
    Real.sqrt (∑ i, (∑ q ∈ s, f q i) ^ 2) ≤ ∑ q ∈ s, Real.sqrt (∑ i, f q i ^ 2) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CumulantEnergy/Basic.lean#L236-L251 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnergy.Basic`, declaration `FunctionalInequalities.KLS.BKL.sqrt_sum_sq_sum_le`; the repository is private at upload time).

View graph