Prove2Me

Quadratic Bound Extends From A Set Closure

Proved
FunctionalInequalities.KLS.LogConcave.norm_sq_le_of_mem_closure_quadratic_bound_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a general Hilbert-space closure lemma.

Let HH be a real inner-product normed space, let z∈Hz\in H, let S⊆HS\subseteq H, and let C∈RC\in\mathbb R. Assume z∈S‾z\in\overline S and, for every w∈Sw\in S,

2⟨z,w⟩−∥w∥2≤C.2\langle z,w\rangle-\|w\|^2\le C.

Then

∥z∥2≤C.\|z\|^2\le C.

The result is reusable for passing variational quadratic inequalities from a dense set to a closure point.

Original Lean declaration header

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

theorem norm_sq_le_of_mem_closure_quadratic_bound
    (z : H) {S : Set H} {C : ℝ} (hz : z ∈ closure S)
    (hbound : ∀ w ∈ S, 2 * ⟪z, w⟫ - ‖w‖ ^ 2 ≤ C) :
    ‖z‖ ^ 2 ≤ C

Module navigation

Module: KLS/LogConcave/BrascampLieb.

Next: inner_center_left_of_mean_zero.

Source excerpt, lines 42–45 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_BrascampLieb

open scoped ContDiff RealInnerProductSpace
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
Formal statement

theorem FunctionalInequalities.KLS.LogConcave.norm_sq_le_of_mem_closure_quadratic_bound_readable
    (z : H) {S : Set H} {C : ℝ} (hz : z ∈ closure S)
    (hbound : ∀ w ∈ S, 2 * ⟪z, w⟫ - ‖w‖ ^ 2 ≤ C) :
    ‖z‖ ^ 2 ≤ C := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/BrascampLieb.lean#L40-L57 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.BrascampLieb`, declaration `FunctionalInequalities.KLS.LogConcave.norm_sq_le_of_mem_closure_quadratic_bound`; the repository is private at upload time).

View graph