Row Contraction Bound for Pair Terms

This formalizes the row-contraction estimate corresponding to BKL (101)–(102).

Let $\nu$ be a compactly supported probability measure on $\mathbb{R}^n$ whose covariance operator $A$ is invertible and strictly positive in every nonzero direction. Let $c,c_2\in\mathbb{N}$, let $\beta\in\mathbb{R}$, and assume that for every $v\in\mathbb{R}^n$,

where $E_j$ is the formalized cumulantEnergy. Then, for every $u\in\mathbb{R}^n$,

The lists in the pair term use the covariance-normalized basis sigmaBasis. This is the one-mask contraction estimate used in the lower-drift bound.

Original Lean declaration header

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

theorem sum_sq_pairTerm_ofFn_le (ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hc : IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support)
    (hA : IsUnit (Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n)))))
    (hApos : ∀ v, v ≠ 0 → 0 < ⟪Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫)
    {c c₂ : ℕ} (β : ℝ)
    (h100 : ∀ v : EuclideanSpace ℝ (Fin n),
      cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) c₂ v ≤
        β * ⟪Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫)
    (u : EuclideanSpace ℝ (Fin n)) :
    ∑ J₁ : Fin c → Fin n, ∑ J₂ : Fin c₂ → Fin n,
      pairTerm (ν : Measure (EuclideanSpace ℝ (Fin n))) u
        (List.ofFn fun i => sigmaBasis (ν : Measure (EuclideanSpace ℝ (Fin n))) (J₁ i))
        (List.ofFn fun i => sigmaBasis (ν : Measure (EuclideanSpace ℝ (Fin n))) (J₂ i)) ≤
      β * cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) (c + 1) u

Module navigation

Module: KLS/BKL/CumulantEnergy/Basic.

Definition modules: Probability/Covariance/Basic.

Supporting theorems: inverseSqrt_mul_mul_inverseSqrt.

Previous: sqrt_sum_sq_sum_le · Next: sqrt_sum_lowerDrift_sq_le_aux.

Source excerpt, lines 385–398 · Frozen source 408915f.