Cumulant Slice Lower Bound From Prescribed Mixed Entries

This auxiliary statement formalizes the Hilbert–Schmidt lower-bound component of Proposition 7.1, p. 28, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), associated with equation (112).

Let $n,N,d\in\mathbb N$ with $N>0$ and $d\ge1$, and $\sigma>0$. Let $\mu$ be any measure on $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), $f:E\to\mathbb R$, and $\nu$ any measure on $H=$ JointSpace $N\ n$, whose coordinate set is $Q=\operatorname{Option}(\operatorname{Fin}N\times\operatorname{Fin}n)$. Denote the coordinate unit vectors by $e_0$ and $e_{(i,j)}$, and the standard basis of $E$ by $b_j$. Write $\kappa_{d+1}^\nu=$ cumulant $\nu\ (d+1)$ and $T_d^\mu f=$ taylorTensor $\mu\ f\ d$.

Assume, for every $I:\operatorname{Fin}d\to\operatorname{Fin}N$ and $J:\operatorname{Fin}d\to\operatorname{Fin}n$,

Then, with $\operatorname{coord}$ denoting coordTensor in the basis $(b_j)$,

This converts the assumed entry identities into a norm lower bound. No probability, integrability, isotropy, or log-concavity hypotheses are imposed on the measures.

Original Lean declaration header

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

theorem sum_sq_cumulant_ge_of_entries {n N : ℕ} (hN : 0 < N) (ν : Measure (JointSpace N n))
    (μ : Measure (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) → ℝ) {σ : ℝ} (hσ : 0 < σ)
    {d : ℕ} (hd : 1 ≤ d)
    (h112 : ∀ (I : Fin d → Fin N) (J : Fin d → Fin n),
      cumulant ν (d + 1) (Fin.cons (EuclideanSpace.single none 1) fun k =>
          EuclideanSpace.single (some (I k, J k)) 1) =
        if ∀ k k', I k = I k' then
          (d.factorial : ℝ) / (σ * Real.sqrt N) *
            taylorTensor μ f d fun k => EuclideanSpace.basisFun (Fin n) ℝ (J k)
        else 0) :
    (d.factorial : ℝ) ^ 2 / σ ^ 2 *
        ‖coordTensor (EuclideanSpace.basisFun (Fin n) ℝ) (taylorTensor μ f d)‖ ^ 2 ≤
      ∑ K : Fin d → Option (Fin N × Fin n),
        cumulant ν (d + 1) (Fin.cons (EuclideanSpace.single none 1) fun k =>
          EuclideanSpace.single (K k) 1) ^ 2

Module navigation

Module: KLS/BKL/Suspension/Cumulant.

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

Supporting theorems: sum_sq_blocks_le.

Next: lintegral_exp_inner_jointLaw.

Source excerpt, lines 30–44 · Frozen source 408915f.