Taylor-Field Recursion With Explicit Constants

Let $V$ be a finite-dimensional real inner-product space with the stated complete, measurable, Borel, and second-countable structures. Let $\nu$ be a log-concave probability measure on $V$, let $m$ be an additive Haar measure, and assume that the interior of the support of $\nu$ is nonempty. Let $U:V\to\mathbb R$ have temperate growth, assume

$$\nu=m.\operatorname{tilted}(-U),$$

and assume that every exponential moment $\int e^{r\|x\|}\,d\nu(x)$ is integrable. Let $C$ be a nonnegative-real parameter satisfying $C_P(\nu)\le C$ and $0<C$.

Assume the Taylor bound that, for every $u\in L^2(\nu)$ and every integer $d\ge1$,

$$\|T_d u\|\le R^d\|u\|,$$

where taylorField and the coordinate tensor are taken in the standard orthonormal basis. Let $f\in L^2(\nu)$ lie in the domain of the adjoint composition of the closed weighted gradient. For integers $k,d$, assume $d\ge1$, $2d\le k+1$, and, for every $j<k$,

$$0<\alpha_j\quad\text{and}\quad \alpha_j^2\le\frac{\beta}{C},$$

where $\alpha_j$ is the corresponding scale of the Poisson iterate.

Then, with defect denoting the iterate defect,

$$\begin{aligned} \|T_d(\nabla_0 h_{k+1})\|^2 &\le \left(\frac{2^{20}\max(1,\beta)^2}{C}\right)^d \|T_{2d}(\nabla_0 h_{k+1-d})\|^2\\ &\quad +(2^{20}\max(1,\beta)^2)^d R^{2d}C \sum_{j\in[k+1-2d,k)}\chi_{j+1}. \end{aligned}$$

This is a technical recursive estimate used to control Taylor fields of Poisson iterates and to feed the later Taylor-coefficient criterion. The explicit constant is part of the statement, rather than an unspecified universal constant.

Formalization Note. The Poincaré constant is compared with the coercion of a NNReal into $\mathbb R$; the displayed inequalities are real-valued. The sum is over Finset.Ico, and the indices and iterates are those represented by taylorField, grad0, iter, scale, and defect.

Original Lean declaration header

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

theorem norm_taylorField_grad0_iter_sq_le (hCpos : 0 < C) {R : ℝ}
    (h29 : ∀ (u : Lp ℝ 2 (ν : Measure V)) (d : ℕ), 1 ≤ d →
      ‖coordTensor (stdOrthonormalBasis ℝ V) (taylorTensor (ν : Measure V) (⇑u) d)‖ ≤
        R ^ d * ‖u‖)
    {f : Lp ℝ 2 (ν : Measure V)} (hf : f ∈ (adjointComp T̄).domain) {β : ℝ} (k d : ℕ)
    (hd : 1 ≤ d) (hdk : 2 * d ≤ k + 1)
    (hα : ∀ j < k, 0 < scale T̄ (iter T̄ f j) ∧ scale T̄ (iter T̄ f j) ^ 2 ≤ β / C) :
    ‖taylorField d (grad0 T̄ (iter T̄ f k))‖ ^ 2 ≤
      (2 ^ 20 * max 1 β ^ 2 / C) ^ d *
          ‖taylorField (2 * d) (grad0 T̄ (iter T̄ f (k - d)))‖ ^ 2 +
        (2 ^ 20 * max 1 β ^ 2) ^ d * R ^ (2 * d) * C *
          ∑ j ∈ Finset.Ico (k + 1 - 2 * d) k, defect T̄ (iter T̄ f j)

Module navigation

Module: KLS/BKL/PoissonIterate/TaylorRecursion.

Definition modules: KLS/BKL/PoissonIterate/Basic, KLS/LogConcave/WeightedGradient/Closure, Analysis/Tensor/Coefficients, Analysis/Tensor/Coordinate, Analysis/Semigroup/AdjointComp, Probability/LogConcave, Analysis/BakryEmery/Tilt/Basic, Poincare/LocalSlope/Basic.

Selected supporting theorems: contDiff_tiltAverage_of_memLp, iteratedFDeriv_comp_perm_of_contDiff, taylorTensor_add, taylorTensor_const_mul, norm_le_four_pow_mul_norm_symmetrize.

Previous: norm_symmetrize_taylorField_grad0_iter_sq_le.

Source excerpt, lines 479–490 · Frozen source 408915f.

Literature

This formalizes Lemma 3.8 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 15, in its route form.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_TaylorRecursion

open MeasureTheory Finset
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Analysis.Tensor
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hUt : U.HasTemperateGrowth)
  (hexp : ∀ r : ℝ, MeasureTheory.Integrable (fun x => Real.exp (r * ‖x‖)) (ν : MeasureTheory.Measure V))
  {C : NNReal} (hC : FunctionalInequalities.Poincare.LocalSlope.Intrinsic.constant ν ≤ (C : ENNReal))
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
include hνU hUt hexp hC

theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.norm_taylorField_grad0_iter_sq_le_readable (hCpos : 0 < C) {R : ℝ}
    (h29 : ∀ (u : Lp ℝ 2 (ν : Measure V)) (d : ℕ), 1 ≤ d →
      ‖coordTensor (stdOrthonormalBasis ℝ V) (taylorTensor (ν : Measure V) (⇑u) d)‖ ≤
        R ^ d * ‖u‖)
    {f : Lp ℝ 2 (ν : Measure V)} (hf : f ∈ (adjointComp T̄).domain) {β : ℝ} (k d : ℕ)
    (hd : 1 ≤ d) (hdk : 2 * d ≤ k + 1)
    (hα : ∀ j < k, 0 < scale T̄ (iter T̄ f j) ∧ scale T̄ (iter T̄ f j) ^ 2 ≤ β / C) :
    ‖taylorField d (grad0 T̄ (iter T̄ f k))‖ ^ 2 ≤
      (2 ^ 20 * max 1 β ^ 2 / C) ^ d *
          ‖taylorField (2 * d) (grad0 T̄ (iter T̄ f (k - d)))‖ ^ 2 +
        (2 ^ 20 * max 1 β ^ 2) ^ d * R ^ (2 * d) * C *
          ∑ j ∈ Finset.Ico (k + 1 - 2 * d) k, defect T̄ (iter T̄ f j) := by sorry