Joint Scalar-Direction Derivative Under Explicit Exponential-Moment Radii

This auxiliary lemma states the scalar-direction derivative of the joint logarithmic Laplace transform under explicit local moment assumptions.

Let $n,N\in\mathbb N$ with $N>0$, $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), $\mu$ a probability measure on $E$, and $f:E\to\mathbb R$ measurable. Let $\beta,r_J,r_G>0$, $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma), and $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$ on $H=$ JointSpace $N\ n$. Let $\Gamma$ be the graph law of $(f(x),x)$ in the Euclidean space indexed by $\operatorname{Option}(\operatorname{Fin}n)$ (Measure.map). Assume:

1. $e^{r_J\|p\|}\in L^1(\lambda)$.
2. $e^{r_G\|y\|}\in L^1(\Gamma)$.

For $z\in H$ with scalar coordinate $z_0=0$ and $\|z\|<\min(r_J,r_G)$, write $z_i\in E$ for its copy blocks and $e_0$ for the scalar coordinate unit vector. Then

Here $\Lambda_\lambda=$ logLaplace and $F_f=$ tiltAverage, the average of $f$ under the exponential tilt at its argument. The conclusion is HasDerivAt, including derivative existence. This local identity requires no regular-potential or isotropy hypothesis.

Original Lean declaration header

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

private theorem joint_first_derivative_of_radii {n N : ℕ} (μ : Measure (EuclideanSpace ℝ (Fin n)))
    [IsProbabilityMeasure μ] {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f)
    {β rJ rG : ℝ} (hβ : 0 < β) (hN : 0 < N) (_hrJ : 0 < rJ) (hrG : 0 < rG)
    (hjoint : Integrable (fun p : JointSpace N n => Real.exp (rJ * ‖p‖))
      (jointLaw μ f β (sigma β) N))
    (hgraph : Integrable (fun y : EuclideanSpace ℝ (Option (Fin n)) => Real.exp (rG * ‖y‖))
      (μ.map (fun x : EuclideanSpace ℝ (Fin n) =>
        (WithLp.toLp 2 fun o => Option.elim o (f x) fun j => x j :
          EuclideanSpace ℝ (Option (Fin n))))))
    (z : JointSpace N n) (hzero : z none = 0) (hz : ‖z‖ < min rJ rG) :
    HasDerivAt (fun w : ℝ => logLaplace (jointLaw μ f β (sigma β) N)
        (w • EuclideanSpace.basisFun (Option (Fin N × Fin n)) ℝ none + z))
      ((∑ i : Fin N, tiltAverage μ f
        (WithLp.toLp 2 fun j => z (some (i, j)))) / (sigma β * Real.sqrt N)) 0

Module navigation

Module: KLS/BKL/Suspension/Derivatives.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, KLS/BKL/Suspension/Law, Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: logLaplace_jointLaw_factorization, laplaceMeasure_mgf, graph_log_integral_hasDerivAt_zero.

Previous: graph_log_integral_hasDerivAt_zero · Next: fderiv_logLaplace_jointLaw_none.

Source excerpt, lines 255–268 · Frozen source 408915f.