Convergence of Integrated Second Differences

Proved

FunctionalInequalities.Analysis.tendsto_integral_secondDifference_mul_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $E$ be a finite-dimensional real inner-product space with its measurable and Borel structures. Let $u:E\to\mathbb R$ be continuous, let $\chi\in C_c^2(E)$ , and let $v\in E$ . As $t\to0^+$ ,

\int_E\frac{u(x+tv)+u(x-tv)-2u(x)}{t^2}\,\chi(x)\,dx \longrightarrow \int_Eu(x)\,D^2\chi(x)[v,v] \,dx.

In Lean, the right-hand integrand is expressed using iteratedFDeriv ℝ 2 χ x (fun _ => v), and the limit is taken along the neighborhood filter $\mathcal N_{>}(0)$ . This is a weak second-order integration identity for compactly supported tests.

Original Lean declaration header

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

theorem tendsto_integral_secondDifference_mul
    {u : E → ℝ} (hu : Continuous u) {χ : E → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ)
    (v : E) :
    Tendsto (fun t : ℝ => ∫ x, (u (x + t • v) + u (x - t • v) - 2 * u x) / t ^ 2 * χ x)
      (𝓝[>] 0) (𝓝 (∫ x, u x * iteratedFDeriv ℝ 2 χ x (fun _ => v)))

Module navigation

Module: Analysis/Convex/SecondOrder.

Previous: subgradient_expansion_of_hasFDerivAt_resolvent · Next: integral_mul_le_integral_mul_sum_iteratedFDeriv.

Source excerpt, lines 390–394 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SecondOrder

open MeasureTheory Set Filter
open scoped Topology
variable {E : Type*}
variable [NormedAddCommGroup E]
variable [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Analysis.tendsto_integral_secondDifference_mul_readable
    {u : E → ℝ} (hu : Continuous u) {χ : E → ℝ} (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ)
    (v : E) :
    Tendsto (fun t : ℝ => ∫ x, (u (x + t • v) + u (x - t • v) - 2 * u x) / t ^ 2 * χ x)
      (𝓝[>] 0) (𝓝 (∫ x, u x * iteratedFDeriv ℝ 2 χ x (fun _ => v))) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/SecondOrder.lean#L388-L430 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.SecondOrder`, declaration `FunctionalInequalities.Analysis.tendsto_integral_secondDifference_mul`; the repository is private at upload time).

View graph