Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

The negative-generator integral pairing

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

Read this first

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

Download module (.lean)
noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ

Exact module and namespace context

Proof roadmap

  1. 1Apply the operator to the second argument

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

  2. 2Negate 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.

Full assumptions and notation

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 verification

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

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.

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)
noncomputable def dirichletForm
    (mu : Measure E) (generator : (E → ℝ) → E → ℝ)
    (f g : E → ℝ) : ℝ :=
  -(∫ x, f x * generator g x ∂mu)

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • MeasureTheory.integral

    Mathematical sources

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