Samplinglib mathematical lesson

Symmetry of the iterated carré du champ

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

Read this first

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

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.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Keep the first term fixed using Γ symmetry
The earlier theorem identifies Γ(f,g) and Γ(g,f), so their images under L agree.
2Swap the remaining terms
After unfolding Γ₂, the other two terms appear in opposite order. Rearranging the subtraction proves the equality pointwise, hence as functions.

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,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 verification

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

Lean proof · iteratedCarreDuChamp_comm

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

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

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.