Construct the algebraic carré du champ

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

Statement

For any type X, any real-linear operator L on real functions on X, and f,g:X→ℝ, define ΓL(f,g) pointwise as one-half the defect between applying L to the product and the two product-rule terms. No measure or topology on X is needed.

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.
• f,g:X→ℝ are arbitrary; products of functions are pointwise.

Construction and meaning

def carreDuChamp
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) : X → ℝ

def carreDuChamp
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) : X → ℝ :=
  fun x => (2 : ℝ)⁻¹ *
    (generator (f * g) x - f x * generator g x - g x * generator f x)

/-- The carre du champ is symmetric in its observable arguments. -/

Scope and omitted-condition boundaries

• No global invariant-law, stationarity for every observable, reversibility, semigroup construction, or concrete diffusion identity is inferred from this declaration.
• No Γ positivity, diffusion chain rule, or gradient formula follows from this definition alone.