ASTIS mathematical exposition

Symmetry of the algebraic carré du champ

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

Statement

For any type X, real-linear L on real functions, and arbitrary f,g:X→ℝ, the functions ΓL(f,g) and ΓL(g,f) are equal everywhere. This symmetry is in the two observable arguments, not symmetry of L with respect to a measure.

\[\Gamma_L(f,g)=\Gamma_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 and g are arbitrary real functions. No measure or stationarity premise.

Mathematical proof

1. Use commutativity of the pointwise product

At every input y, f(y)g(y)=g(y)f(y), hence the input functions fg and gf are equal.

\[fg=gf\quad\Longrightarrow\quad L(fg)=L(gf).\]

Corresponding Lean step

funext y; mul_comm

2. Reorder the two subtraction terms

At each x, the first operator term is unchanged and the two cross terms exchange places. Real arithmetic gives identical values.

\[\tfrac12[L(fg)-fLg-gLf]=\tfrac12[L(gf)-gLf-fLg].\]

Corresponding Lean step

funext x; simp only [carreDuChamp, hfg]; ring

Lean statement · carreDuChamp_comm

The conclusion is equality of functions. It does not say ∫f Lg=∫g Lf; no measure even appears.

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 carreDuChamp_comm
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) :
    carreDuChamp generator f g = carreDuChamp generator g f

Exact module and namespace context

Lean proof · carreDuChamp_comm

The proof first establishes equality of the pointwise product inputs, then unfolds Γ at an arbitrary state and rearranges the real terms.

theorem carreDuChamp_comm
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) :
    carreDuChamp generator f g = carreDuChamp generator g f := by
  funext x
  have hfg : f * g = g * f := by
    funext y
    exact mul_comm (f y) (g y)
  simp only [carreDuChamp, hfg]
  ring

/-- Chewi Definition 1.2.28: the iterated carre du champ. -/

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.
Argument symmetry of Γ is not reversibility or self-adjointness of L. No positivity claim is made.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp.carreDuChamp

Mathlib API called (external library)

mul_comm

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.