Quadratic test function at a point

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For $A\in\mathbb{R}^{n\times n}$ , $x_0,b,x\in\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin} n)$ , and $c\in\mathbb{R}$ , quadraticAt A x₀ b c x is $c+\langle b,x-x_0\rangle+\frac12\langle x-x_0,A(x-x_0)\rangle$ . It is the quadratic test used in the weak Alexandrov and viscosity development, which also contains push-forward and geometric auxiliary results.

Original module imports

import FunctionalInequalities.Analysis.Convex.Subgradient
import Mathlib

Original declaration excerpt

Shown in the original module context.

def quadraticAt {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ)
    (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  c + ⟪b, x - x₀⟫ + (1 / 2) * ⟪x - x₀, Matrix.toEuclideanLin A (x - x₀)⟫

Module navigation

Direct project imports: Analysis/Convex/Subgradient.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Convex.Alexandrov · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Subgradient
import Mathlib

noncomputable section
open MeasureTheory Set
open scoped RealInnerProductSpace ENNReal
section LT12C1QuadraticSubgradientImage
open MeasureTheory Set Matrix
open scoped RealInnerProductSpace ENNReal
namespace FunctionalInequalities
namespace Analysis
/-- The quadratic function with constant `c`, slope `b` and Hessian matrix `A` centred at `x₀`:
`Q x = c + ⟪b, x − x₀⟫ + ½ ⟪x − x₀, A (x − x₀)⟫` (weak Letwin route, viscosity tests). -/
def quadraticAt {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x₀ b : EuclideanSpace ℝ (Fin n)) (c : ℝ)
    (x : EuclideanSpace ℝ (Fin n)) : ℝ :=
  c + ⟪b, x - x₀⟫ + (1 / 2) * ⟪x - x₀, Matrix.toEuclideanLin A (x - x₀)⟫
end Analysis
end FunctionalInequalities
end LT12C1QuadraticSubgradientImage

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Alexandrov.lean#L1414-L1418 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Alexandrov`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov`; the repository is private at upload time).

View graph