The positive-parameter Bakry–Émery condition

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.SatisfiesBakryEmery · def · Teaching coverage

Statement

For a real-linear operator L on real functions on an arbitrary type X and a real α, SatisfiesBakryEmery L α means α>0 and Γ₂,L(f,f)(x)≥α ΓL(f,f)(x) for every real-valued function f and every state x. The formal predicate quantifies over all functions, with no hidden admissible-observable domain.

All objects and hypotheses

• X is an arbitrary type, with no measurable-space, topological-space, normed-space, or finiteness hypothesis.
• L:(X→ℝ)→ₗ[ℝ](X→ℝ) is a real-linear operator on all real-valued functions on X. No Markov semigroup or invariant law is supplied.
• α is any real input to the predicate; strict positivity is one of its required conjuncts.
• No measure, regularity domain, probability law, or topology on X is present.

Construction and meaning

def SatisfiesBakryEmery
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (alpha : ℝ) : Prop

def SatisfiesBakryEmery
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (alpha : ℝ) : Prop :=
  0 < alpha ∧ ∀ (f : X → ℝ) (x : X),
    alpha * carreDuChamp generator f f x ≤
      iteratedCarreDuChamp generator f f x

/-- Chewi Lemma 1.2.13: the Markov-semigroup Jensen inequality implies
nonnegativity of the carre du champ after taking the right-generator limit.

The theorem is pointwise.  `hf` and `hf2` are the actual right difference-
quotient limits for `f` and `f²`; `hcontinuous` is strong/right continuity of
the orbit at the selected state. -/

Scope and omitted-condition boundaries

• This defines a proposition that must be proved for a concrete model. It does not prove existence of a witness or derive an inequality from the operator's name.
• No global invariant-law, stationarity for every observable, reversibility, semigroup construction, or concrete diffusion identity is inferred from this declaration.
• This does not prove a Bakry–Émery criterion for LSI/Poincaré, a lower Ricci/Hessian bound, or a nontrivial ergodic property. The zero-operator test illustrates that no such additional structure is encoded.