ASTIS mathematical exposition

Construct the iterated carré du champ

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

Statement

For any type X, real-linear L on real functions, and observables f,g, define Γ₂,L(f,g) as half of L applied to ΓL(f,g), minus the two mixed terms ΓL(f,Lg) and ΓL(g,Lf). This uses only the previously defined algebraic Γ.

\[\Gamma_{2,L}(f,g):=\frac12\big[L(\Gamma_L(f,g))-\Gamma_L(f,Lg)-\Gamma_L(g,Lf)\big].\]

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. Γ is the same normalized expression defined previously.

Construction and meaning

1. Build the three observable functions

Apply L to Γ(f,g), and substitute Lg or Lf into the appropriate Γ argument.

\[A:=L(\Gamma_L(f,g)),\quad B:=\Gamma_L(f,Lg),\quad C:=\Gamma_L(g,Lf).\]

Corresponding Lean step

CarreDuChamp.carreDuChamp; generator

2. Take the normalized difference

Combine those functions pointwise with the same factor one-half.

\[\Gamma_{2,L}(f,g)=\tfrac12(A-B-C).\]

Corresponding Lean step

CarreDuChamp.iteratedCarreDuChamp

Lean statement · iteratedCarreDuChamp

The result is a real-valued function on X. The subscript two denotes this algebraic iterate; no Hessian or second-order differentiability assumption is encoded.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

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

Exact module and namespace context

Lean construction · iteratedCarreDuChamp

This construction applies L and Γ in the displayed arrangement and combines their real values. There is no curvature estimate to prove at this stage.

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

/-- The iterated carre du champ inherits symmetry from the first one. -/

Exact module and namespace context

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 nonnegativity of Γ₂, curvature lower bound, Bochner identity, or concrete diffusion/Hessian identification is asserted.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp

Mathlib API called (external library)

LinearMap

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Existing source-correspondence record: chewi-1-2-definition-1-2-28 — Existing local record for Chewi Definition1.2.28, edition2026-08-09, printed p.18/PDF p.30. Reported only within the current declaration's explicit assumptions; no new source audit or source-equivalence verdict.
Existing focused test — Declaration-visibility #check. No test/build run for this packet.
Existing focused test — Algebraic example proves Γ₂=0 for the zero operator. No test/build run for this packet.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.