Transfer of Cumulant Energy Through Standardization

This auxiliary statement transfers an isotropic cumulant bound to a compact posterior.

Let $\mu$ be a compactly supported isotropic log-concave probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$. Let $c\in E$ and let $Q$ be self-adjoint and positive semidefinite. Assume $d\ge1$ and suppose that every compactly supported isotropic log-concave law satisfies

Then every $v\in E$ satisfies

This is a technical transport lemma and does not itself provide the assumed constant $b$.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

private theorem posterior_energy_transfer
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
    (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (c : EuclideanSpace ℝ (Fin n))
    (Q : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hSym : IsSelfAdjoint Q) (hQ : ∀ x, 0 ≤ ⟪Q x, x⟫)
    {d : ℕ} (hd : 1 ≤ d) {b : ℝ}
    (h : ∀ ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
      KLS.LogConcave ν → KLS.Isotropic ν →
      IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support →
      ∀ u : EuclideanSpace ℝ (Fin n),
        ∑ J : Fin d → Fin n,
          cumulant (ν : Measure (EuclideanSpace ℝ (Fin n))) (d + 1)
            (Fin.cons u fun k => EuclideanSpace.basisFun (Fin n) ℝ (J k)) ^ 2 ≤
          b * ‖u‖ ^ 2)
    (v : EuclideanSpace ℝ (Fin n)) :
    cumulantEnergy (compactPosterior μ hc c Q : Measure (EuclideanSpace ℝ (Fin n))) d v ≤
      b * ⟪Covariance.operator
        (compactPosterior μ hc c Q : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫

Module navigation

Module: KLS/BKL/Localization/Energy/Bound.

Definition modules: KLS/BKL/CumulantEnergy/Basic, Probability/Covariance/Basic, Probability/LogConcave, KLS/Isotropic, Analysis/BakryEmery/Cumulant/Basic, Probability/Posterior/CompactDomain.

Selected supporting theorems: cumulant_map_affine, inverseSqrt_mul_mul_inverseSqrt, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, Isotropic.exists_inverseSqrt_equiv_isotropic_standardized, logConcave_of_concave_tilt.

Next: norm_posteriorMean_le.

Source excerpt, lines 24–43 · Frozen source 408915f.