Symmetric average in Euclidean space

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Viscosity

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For $g:\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin} n)\to\mathbb{R}$ and $h,y$ in that space, n9_average g h y is the symmetric average $\frac12\bigl(g(y+h)+g(y-h)\bigr)$ . It is a private helper in the touching-test and viscosity-inequality development.

Original module imports

import FunctionalInequalities.Analysis.BakryEmery.HessianOperator
import Mathlib.Analysis.Calculus.DerivativeTest
import FunctionalInequalities.Analysis.Convex.Alexandrov
import FunctionalInequalities.Analysis.Convex.SecondOrder
import FunctionalInequalities.Analysis.Matrix.LogDet
import Mathlib.Analysis.Calculus.BumpFunction.Convolution

Original declaration excerpt

Shown in the original module context.

private def n9_average {n : ℕ} (g : EuclideanSpace ℝ (Fin n) → ℝ)
    (h y : EuclideanSpace ℝ (Fin n)) : ℝ :=
  (1 / 2 : ℝ) * (g (y + h) + g (y - h))

Module navigation

Direct project imports: Analysis/BakryEmery/HessianOperator, Analysis/Convex/Alexandrov, Analysis/Convex/SecondOrder, Analysis/Matrix/LogDet.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator
import Mathlib.Analysis.Calculus.DerivativeTest
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SecondOrder
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_LogDet
import Mathlib.Analysis.Calculus.BumpFunction.Convolution

noncomputable section
open Set Metric Filter
open scoped RealInnerProductSpace Topology
open FunctionalInequalities.Probability.Stein
section LT17BMaximumWithComparison
open MeasureTheory Set Metric Filter
open scoped RealInnerProductSpace ENNReal Topology
open FunctionalInequalities.Probability.Stein
namespace FunctionalInequalities
namespace Analysis
 def n9_average {n : ℕ} (g : EuclideanSpace ℝ (Fin n) → ℝ)
    (h y : EuclideanSpace ℝ (Fin n)) : ℝ :=
  (1 / 2 : ℝ) * (g (y + h) + g (y - h))
end Analysis
end FunctionalInequalities
end LT17BMaximumWithComparison

Source

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

View graph