Prove2Me

Extended-Valued Young Inequality for Squared Sums

Proved
FunctionalInequalities.Energy.sq_add_le_mul_sq_add_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement is a parameterized Young inequality in [0,∞][0,\infty].

Let θ∈[0,∞)\theta\in[0,\infty) satisfy 0<θ0<\theta, and let x,y∈[0,∞]x,y\in[0,\infty] be ENNReal values. Then

(x+y)2≤(1+θ)x2+(1+θ−1)y2.(x+y)^2 \leq (1+\theta)x^2+(1+\theta^{-1})y^2.

The inequality remains valid when x=∞x=\infty or y=∞y=\infty; the inverse is the ENNReal inverse of the positive parameter. This auxiliary estimate is used to separate a principal local-slope term from a cutoff-error term.

Original Lean declaration header

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

theorem sq_add_le_mul_sq_add {θ : ℝ≥0} (hθ : 0 < θ) (x y : ℝ≥0∞) :
    (x + y) ^ 2 ≤ (1 + (θ : ℝ≥0∞)) * x ^ 2 + (1 + (θ : ℝ≥0∞)⁻¹) * y ^ 2

Module navigation

Module: Energy/Euclidean/Slope/Density.

Previous: relaxation_le_localSlope_of_lipschitzWith · Next: relaxation_le_localSlope_of_admissible.

Source excerpt, lines 982–983 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Density

open scoped ENNReal NNReal ContDiff
universe u
Formal statement

theorem FunctionalInequalities.Energy.sq_add_le_mul_sq_add_readable {θ : ℝ≥0} (hθ : 0 < θ) (x y : ℝ≥0∞) :
    (x + y) ^ 2 ≤ (1 + (θ : ℝ≥0∞)) * x ^ 2 + (1 + (θ : ℝ≥0∞)⁻¹) * y ^ 2 := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Euclidean/Slope/Density.lean#L981-L1009 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Euclidean.Slope.Density`, declaration `FunctionalInequalities.Energy.sq_add_le_mul_sq_add`; the repository is private at upload time).

View graph