Smoothness of Tilt Averages of $L^2$ Functions

This formalizes the smoothness part of the tilt-average framework in Bizeul–Klartag–Lehec, Equations (26)–(28), p. 9.

Let $E$ be a finite-dimensional real inner-product space with Borel structure, let $\mu$ be a finite nonzero measure, and assume every exponential norm moment is finite:

$$\forall r\in\mathbb R, \quad \int e^{r\|x\|}\,d\mu(x)<\infty.$$

For any real-valued $f\in L^2(\mu)$, the tilt average

$$F_f(z)=\int f(x)\,d\mu_z(x)$$

is smooth on all of $E$:

$$F_f\in C^\infty(E).$$

Here tiltAverage μ f is defined using the exponentially tilted measure. The conclusion is global smoothness, not merely smoothness near the origin.

Original Lean declaration header

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

theorem contDiff_tiltAverage_of_memLp (μ : Measure E) [IsFiniteMeasure μ] [NeZero μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {f : E → ℝ} (hf : MemLp f 2 μ) :
    ContDiff ℝ ∞ (tiltAverage μ f)

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: integrable_exp_mul_norm_of_memLp.

Previous: integrable_exp_mul_norm_of_memLp · Next: taylorTensor_add.

Source excerpt, lines 304–306 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_SquareIntegrable

open MeasureTheory Filter Topology FunctionalInequalities.Analysis.Tensor
open scoped RealInnerProductSpace ContDiff ENNReal
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E]

theorem FunctionalInequalities.Analysis.BakryEmery.contDiff_tiltAverage_of_memLp_readable (μ : Measure E) [IsFiniteMeasure μ] [NeZero μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {f : E → ℝ} (hf : MemLp f 2 μ) :
    ContDiff ℝ ∞ (tiltAverage μ f) := by sorry