Mean Gradient Square and First Taylor Tensor

This formalizes BKL (49) for tensor fields.

Let $V$ be finite-dimensional and let $\nu=m\mathbin{.}\mathrm{tilted}(-U)$, where $U\in C^2$ and all exponential moments of $\nu$ are integrable. Let $h$ be a field at level $k$, and assume every component of $h$ belongs to the domain of $A=\bar T^\dagger\bar T$. Then the squared sum of the means of the gradient components equals the squared norm of the first Taylor field of the generator field:

Here meanGradSq sums the squared norms of the component means, genField applies the generator componentwise, and taylorField 1 is the corresponding first Taylor coefficient array.

This identifies the first gradient-drop quantity with a Taylor-tensor norm in the iterate analysis.

Formalization Note: The equality is in real numbers; all field components are $L^2(\nu)$ classes and the domain assumption is componentwise.

Original Lean declaration header

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

theorem meanGradSq_eq_norm_taylorField_one_genField {k : ℕ} (h : Field ν k)
    (hh : ∀ I, h I ∈ (adjointComp T̄).domain) :
    meanGradSq T̄ h = ‖taylorField 1 (genField T̄ h)‖ ^ 2

Module navigation

Module: KLS/BKL/PoissonIterate/Taylor.

Definition modules: KLS/BKL/PoissonIterate/Basic, KLS/LogConcave/WeightedGradient/Closure, Analysis/Tensor/Coordinate, Analysis/Semigroup/AdjointComp, Probability/LogConcave.

Supporting theorems: taylorTensor_gen_apply.

Previous: symmetrize_taylorField_grad0_step · Next: sum_mean_partialDeriv_sq_le.

Source excerpt, lines 315–317 · Frozen source 408915f.