Prove2Me

Inverse Quadratic Young Inequality

Proved
FunctionalInequalities.Analysis.inverse_quadratic_young_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the inverse-quadratic inequality cited as Lemma A.6 of Letwin (arXiv:2607.24164v1).

Let ι be a finite index type with decidable equality, let H be a real positive-definite matrix, and let v,w:ι→ℝ. Then

2 v⋅w≤v⋅(H−1v)+w⋅(Hw).2\,v\mathbin{\cdot}w\leq v\mathbin{\cdot}(H^{-1}v)+w\mathbin{\cdot}(Hw).

This is a finite-dimensional quadratic Young inequality with no identity or commutation restriction on H.

The result is a standard algebraic estimate for inverse-weighted cross terms.

Original Lean declaration header

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

theorem inverse_quadratic_young
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (H : Matrix ι ι ℝ) (hH : H.PosDef) (v w : ι → ℝ) :
    2 * (v ⬝ᵥ w) ≤ v ⬝ᵥ (H⁻¹ *ᵥ v) + w ⬝ᵥ (H *ᵥ w)

Module navigation

Module: Analysis/Matrix/Positivity.

Previous: root_difference_bound · Next: trace_mul_nonneg.

Source excerpt, lines 292–295 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity

open scoped BigOperators Matrix
Formal statement

theorem FunctionalInequalities.Analysis.inverse_quadratic_young_readable
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (H : Matrix ι ι ℝ) (hH : H.PosDef) (v w : ι → ℝ) :
    2 * (v ⬝ᵥ w) ≤ v ⬝ᵥ (H⁻¹ *ᵥ v) + w ⬝ᵥ (H *ᵥ w) := by sorry
Source
Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma A.6. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/Positivity.lean#L291-L334 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Positivity`, declaration `FunctionalInequalities.Analysis.inverse_quadratic_young`; the repository is private at upload time).

View graph