Samplinglib mathematical lesson

Symmetry of the algebraic carré du champ

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

Read this first

Mathematical 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).\]

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.

Download module (.lean)

theorem carreDuChamp_comm
    (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ) :
    carreDuChamp generator f g = carreDuChamp generator g f

Exact module and namespace context

Proof roadmap

1Use 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.
2Reorder 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.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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