A-Priori Posterior Cumulant Energy Bound

This statement gives an a-priori bound on posterior cumulant energies along the localization parameter space.

Let $\mu$ be a compactly supported isotropic log-concave probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$. Let $r\ge0$ and assume

For every $d\in\mathbb{N}$, there exists $C\ge0$ such that for every parameter $p=(c,Q)$ with $Q$ self-adjoint and positive semidefinite, and every $u$, the compact posterior satisfies

The constant may depend on $\mu$, $r$, and $d$. This is a finite-dimensional posterior control statement used to justify integrability and localization estimates.

Original Lean declaration header

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

theorem exists_cumulantEnergy_le (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ) {r : ℝ} (hr : 0 ≤ r)
    (hsupp : (μ : Measure (EuclideanSpace ℝ (Fin n))).support ⊆ Metric.closedBall 0 r) (d : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ p : Param n, IsSelfAdjoint p.2 → (∀ x, 0 ≤ ⟪p.2 x, x⟫) →
      ∀ u : EuclideanSpace ℝ (Fin n),
        cumulantEnergy (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) d u ≤ C * ‖u‖ ^ 2

Module navigation

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

Definition modules: KLS/BKL/CumulantEnergy/Basic, KLS/BKL/Localization/Coefficients, Probability/LogConcave, KLS/Isotropic, Probability/Posterior/CompactDomain.

Selected supporting theorems: tiltAverage_inner_eq_fderiv_logLaplace, norm_posteriorMean_le, exists_sum_sq_cumulant_le_isotropic, opNorm_covariance_compactPosterior_le_sq_radius, exists_uniform_norm_moments_tilted_quadraticExponent_of_compact.

Previous: norm_posteriorMean_le.

Source excerpt, lines 193–197 · Frozen source 408915f.