ASTIS mathematical exposition

Symmetry of the iterated carré du champ

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.iteratedCarreDuChamp_comm · theorem · Teaching coverage

Statement

For any type X, real-linear L on real-valued functions, and arbitrary f,g, the functions Γ₂,L(f,g) and Γ₂,L(g,f) agree at every state.

\[\Gamma_{2,L}(f,g)=\Gamma_{2,L}(g,f).\]

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. No measure, topology, or curvature premise.

Mathematical proof

1. Keep the first term fixed using Γ symmetry

The earlier theorem identifies Γ(f,g) and Γ(g,f), so their images under L agree.

\[L(\Gamma_L(f,g))=L(\Gamma_L(g,f)).\]

Corresponding Lean step

CarreDuChamp.carreDuChamp_comm

2. Swap the remaining terms

After unfolding Γ₂, the other two terms appear in opposite order. Rearranging the subtraction proves the equality pointwise, hence as functions.

\[\tfrac12[A-\Gamma_L(f,Lg)-\Gamma_L(g,Lf)]=\tfrac12[A-\Gamma_L(g,Lf)-\Gamma_L(f,Lg)].\]

Corresponding Lean step

funext x; simp only [iteratedCarreDuChamp, carreDuChamp_comm]; ring

Lean statement · iteratedCarreDuChamp_comm

This is symmetry in the two observable slots, not an integral or spectral symmetry statement.

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.

theorem iteratedCarreDuChamp_comm
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) :
    iteratedCarreDuChamp generator f g =
      iteratedCarreDuChamp generator g f

Exact module and namespace context

Lean proof · iteratedCarreDuChamp_comm

The proof unfolds the iterate, reuses symmetry of Γ for its operator input, and rearranges the two real cross terms.

theorem iteratedCarreDuChamp_comm
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) :
    iteratedCarreDuChamp generator f g =
      iteratedCarreDuChamp generator g f := by
  funext x
  simp only [iteratedCarreDuChamp, carreDuChamp_comm]
  ring

/-- Chewi Definition 1.2.29: the curvature-dimension condition
`CD(alpha, infinity)`, including the source requirement `alpha > 0`. -/

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 curvature or integrated nonnegativity follows merely from this argument symmetry.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in 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.