Operator Norm Controlled by a Bilinear Form

Proved

FunctionalInequalities.KLS.LogConcave.Suspension.opNorm_le_of_inner_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a technical operator-norm estimate.

Let $E$ be a complete real inner-product normed space, let $A:E\to E$ be continuous linear, and let $\kappa$ be a continuous bilinear form on $E$ . Suppose that for all $u,v\in E$ ,

\langle Au,v\rangle=\kappa(u,v).

Then

\|A\|\le\|\kappa\|.

Here the norm on $\kappa$ is the continuous multilinear-map norm. The lemma provides a reusable way to transfer estimates on a bilinear representation to the associated operator.

Original Lean declaration header

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

theorem opNorm_le_of_inner_eq
    [CompleteSpace E]
    {A : E →L[ℝ] E}
    {κ : ContinuousMultilinearMap ℝ (fun _ : Fin 2 => E) ℝ}
    (h : ∀ u v : E, ⟪A u, v⟫ = κ ![u, v]) : ‖A‖ ≤ ‖κ‖

Module navigation

Module: KLS/BKL/CompactReduction.

Previous: norm_sub_one_le_of_isPositive_mul_self · Next: inner_self_pos_of_norm_sub_one_lt.

Source excerpt, lines 146–150 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CompactReduction

open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.Suspension.opNorm_le_of_inner_eq_readable
    [CompleteSpace E]
    {A : E →L[ℝ] E}
    {κ : ContinuousMultilinearMap ℝ (fun _ : Fin 2 => E) ℝ}
    (h : ∀ u v : E, ⟪A u, v⟫ = κ ![u, v]) : ‖A‖ ≤ ‖κ‖ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CompactReduction.lean#L145-L163 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CompactReduction`, declaration `FunctionalInequalities.KLS.LogConcave.Suspension.opNorm_le_of_inner_eq`; the repository is private at upload time).

View graph