ASTIS mathematical exposition

The negative-generator integral pairing

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.dirichletForm · def · Teaching coverage

Statement

For a measure μ on a measurable space E, an arbitrary operator L on real-valued functions, and observables f,g:E→ℝ, define the generator Dirichlet pairing to be minus the μ-integral of f times Lg. No symmetry, positivity or operator linearity is part of this definition.

\[\mathcal E_\mu^L(f,g):=-\int_E f(x)(Lg)(x)\,d\mu(x).\]

All objects and hypotheses

E is any measurable space and μ is any measure on E, unless probability normalization is explicitly included below. No topology, norm, finite dimension, σ-finiteness, or nonempty-space premise is imposed.
L:(E→ℝ)→(E→ℝ) is an arbitrary operator on real functions. This signature does not require linearity, measurability preservation, Markovness, or a semigroup.
f,g:E→ℝ are arbitrary; no integrability premise.

Construction and meaning

1. Apply the operator to the second argument

First form the function Lg and multiply its value by the first observable f.

\[u(x):=f(x)(Lg)(x).\]

Corresponding Lean step

generator g; pointwise real multiplication

2. Negate its integral

The definition fixes the negative-generator sign convention. With integrability, this is the usual finite pairing; without it the real integral remains totalized.

\[\mathcal E_\mu^L(f,g)=-\int_Eu\,d\mu.\]

Corresponding Lean step

MeasureTheory.integral; Generator.dirichletForm

Lean statement · dirichletForm

The operator parameter is a function taking functions to functions; it is not a linear-map parameter. The return value is a real number, not a bilinear-form structure with proved laws.

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.

noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ

Exact module and namespace context

Lean construction · dirichletForm

This is a construction only: apply L to g, multiply by f, integrate, and negate. No integration-by-parts, symmetry or nonnegativity proof occurs.

noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ :=
  -(∫ x, f x * generator g x ∂mu)

/-- Variance as the squared centered `L2(mu)` norm. -/

Exact module and namespace context

Scope and omitted-condition boundaries

All integrals are real Bochner integrals. An integral is totalized to zero when its integrand is not integrable; writing the integral does not prove a genuine finite expectation or energy.
No global invariant-law, stationarity for every observable, reversibility, semigroup construction, or concrete diffusion identity is inferred from this declaration.
Calling this a Dirichlet form does not assert bilinearity, closedness, positivity, or a Hilbert-space form domain.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral

Mathematical sources

Exact existing ASTIS declaration — Current statement and body; renderer extracts exact Lean rather than duplicating it in this packet.
Totalized Bochner integral — integral_undef explains the nonintegrable case; it is background, not a call in this definition.
Existing focused test — Declaration-visibility #check only. No test/build run for 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.