Samplinglib mathematical lesson

Nonnegative Γ gives a nonnegative quadratic generator pairing

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

Read this first

Mathematical statement

Let X be a measurable space, μ any measure, L a real-linear operator on real functions and f:X→ℝ. Assume L(f²) and fLf are μ-integrable, ∫L(f²)dμ=0, and ΓL(f,f)(x)≥0 for every x∈X. Then the negative-generator quadratic pairing Eμ^L(f,f) is nonnegative. No separate symmetry premise is required on the diagonal.

\[\begin{gathered}L(f^2),fLf\in L^1(\mu),\qquad\int_XL(f^2)\,d\mu=0,\qquad\forall x,\ \Gamma_L(f,f)(x)\ge0\\\Longrightarrow\quad0\le\mathcal E_\mu^L(f,f)=-\int_X fLf\,d\mu.\end{gathered}\]

Lean statement · negativeGenerator_quadratic_nonneg

The repeated observable removes the need for a separate pair-symmetry proof. Positivity of Γ is nevertheless a supplied pointwise hypothesis; the theorem does not derive it from a Markov operator.

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 negativeGenerator_quadratic_nonneg
    [MeasurableSpace X]
    (mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f : X → ℝ)
    (hLf2 : Integrable (generator (f * f)) mu)
    (hfLf : Integrable (fun x => f x * generator f x) mu)
    (hstationary : (∫ x, generator (f * f) x ∂mu) = 0)
    (hgamma : ∀ x, 0 ≤ carreDuChamp generator f f x) :
    0 ≤ FunctionalInequalities.Generator.dirichletForm mu generator f f

Exact module and namespace context

Proof roadmap

1Specialize the previous theorem to the repeated observable
Use f in both slots. The two cross integrability obligations are the same supplied hfLf, and the symmetry equation becomes reflexive.
2Pass the pointwise sign condition to an a.e. one
A statement true at every x is true μ-almost everywhere, whatever μ is.
3Integrate nonnegativity
The real integral of an a.e. nonnegative function is nonnegative. Combine this with the diagonal pairing identity.

Full assumptions and notation

All objects and hypotheses

X is any measurable space and μ any measure on X; no probability, finite-mass, σ-finiteness, or topological premise.
L:(X→ℝ)→ₗ[ℝ](X→ℝ) is a real-linear operator on all real-valued functions on X. No Markov semigroup or invariant law is supplied.
f:X→ℝ is arbitrary. hLf2 proves Integrable L(f*f) μ and hfLf proves Integrable (fLf) μ.
hstationary is only ∫L(f*f)dμ=0. hgamma is pointwise nonnegativity ΓL(f,f)(x)≥0 for every x, not merely an a.e. assumption in the stated theorem.

Mathematical proof

1. Specialize the previous theorem to the repeated observable

Use f in both slots. The two cross integrability obligations are the same supplied hfLf, and the symmetry equation becomes reflexive.

\[\mathcal E_\mu^L(f,f)=\int_X\Gamma_L(f,f)\,d\mu.\]

Corresponding Lean step

CarreDuChamp.fundamental_integration_by_parts mu generator f f hLf2 hfLf hfLf hstationary rfl

2. Pass the pointwise sign condition to an a.e. one

A statement true at every x is true μ-almost everywhere, whatever μ is.

\[\forall x,\ \Gamma_L(f,f)(x)\ge0\Longrightarrow\Gamma_L(f,f)\ge0\quad\mu\text{-a.e.}.\]

Corresponding Lean step

Filter.Eventually.of_forall hgamma

3. Integrate nonnegativity

The real integral of an a.e. nonnegative function is nonnegative. Combine this with the diagonal pairing identity.

\[0\le\int_X\Gamma_L(f,f)\,d\mu=\mathcal E_\mu^L(f,f).\]

Corresponding Lean step

MeasureTheory.integral_nonneg_of_ae

Lean verification

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

Lean proof · negativeGenerator_quadratic_nonneg

Apply the already-proved integration-by-parts identity on the diagonal, using the same pairing-integrability proof twice. Then integrate the supplied nonnegative Γ and rewrite the result as the quadratic pairing.

Download module (.lean)

theorem negativeGenerator_quadratic_nonneg
    [MeasurableSpace X]
    (mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f : X → ℝ)
    (hLf2 : Integrable (generator (f * f)) mu)
    (hfLf : Integrable (fun x => f x * generator f x) mu)
    (hstationary : (∫ x, generator (f * f) x ∂mu) = 0)
    (hgamma : ∀ x, 0 ≤ carreDuChamp generator f f x) :
    0 ≤ FunctionalInequalities.Generator.dirichletForm mu generator f f := by
  have hibp := fundamental_integration_by_parts mu generator f f
    hLf2 hfLf hfLf hstationary rfl
  rw [hibp.2]
  exact integral_nonneg_of_ae (Filter.Eventually.of_forall hgamma)

end CarreDuChamp
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

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 global reversibility or self-adjointness is proved. The conclusion concerns this one observable satisfying the listed local assumptions.
The Jensen-to-generator theorem is a possible separate producer of hgamma, but this proof does not call it or establish its limit hypotheses.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Filter.Eventually.of_forall
MeasureTheory.integral_nonneg_of_ae

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-corollary-1-2-15 — Existing local record for Chewi Corollary1.2.15, edition2026-08-09, printed p.14/PDF p.26. Reported only within the current declaration's explicit assumptions; no new source audit or source-equivalence verdict.
Nonnegative a.e. Bochner integrands — Exact final positivity theorem.
Existing focused test — Declaration-visibility #check only; the Γ-positivity premise remains supplied. No test/build run for 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.