Cumulant Energy Generator Chain Rule

This is the chain-rule expression for the generator of the posterior cumulant energy.

Let $\mu$ be an isotropic probability measure on $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ with compact support. Let $r\in\mathbb N$ satisfy $2\le r$, let $u$ be a direction, and let $p=(c,Q)$ be a localization parameter. Define $E_r(p,u)=\operatorname{cumulantEnergy}(\mu_p,r,u)$, and write energyForm for the quadratic form applied to the covariance-coordinate tensor and cumulant tensor. The identity uses energyTensor, lowerTensor, noiseTensor, and conjugatedNoiseOperator.

The equality is a technical generator decomposition in conjugated coordinates. It isolates the drift and noise derivatives needed for subsequent energy inequalities; it does not itself assert a lower bound.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem generator_cumulantEnergy_eq (hiso : KLS.Isotropic μ) {r : ℕ} (hr : 2 ≤ r)
    (u : EuclideanSpace ℝ (Fin n)) (p : Param n) :
    generator μ hc
        (fun q : Param n => cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) r u) p =
      fderiv ℝ (fun q : (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) × ((Fin r → Fin n) → ℝ) =>
          energyForm q.1 q.2) (1, energyTensor μ hc p r u)
          (-1, -(((r : ℝ) + 1) • energyTensor μ hc p r u + lowerTensor μ hc p r u)) +
        (1 / 2 : ℝ) * ∑ k, fderiv ℝ (fderiv ℝ
          (fun q : (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) × ((Fin r → Fin n) → ℝ) =>
            energyForm q.1 q.2)) (1, energyTensor μ hc p r u)
          (conjugatedNoiseOperator μ hc p k, noiseTensor μ hc p r u k)
          (conjugatedNoiseOperator μ hc p k, noiseTensor μ hc p r u k)

Module navigation

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

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

Selected supporting theorems: contDiffAt_energyForm, inner_self_pos_of_isPositive_of_isUnit, inverseSqrt_mul_mul_inverseSqrt, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, contDiff_cumulant_posterior.

Previous: stdMatrix_conjugatedNoiseOperator · Next: generator_cumulantEnergy_ge.

Source excerpt, lines 251–263 · Frozen source 408915f.