ASTIS mathematical exposition

Pairwise integration by parts from three integrable terms

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

Statement

Let X be a measurable space, μ any measure, L a real-linear operator on real functions, and f,g:X→ℝ. Assume L(fg), fLg and gLf are μ-integrable; ∫L(fg)dμ=0; and ∫fLg dμ=∫gLf dμ. Then the two Dirichlet pairings agree and their common value equals ∫ΓL(f,g)dμ. Stationarity and symmetry are required only for these displayed observables and integrals.

\[\begin{gathered}L(fg),fLg,gLf\in L^1(\mu),\qquad\int_XL(fg)\,d\mu=0,\qquad\int_XfLg\,d\mu=\int_XgLf\,d\mu\\\Longrightarrow\quad\mathcal E_\mu^L(f,g)=\mathcal E_\mu^L(g,f),\qquad\mathcal E_\mu^L(f,g)=\int_X\Gamma_L(f,g)\,d\mu.\end{gathered}\]

All objects and hypotheses

X is any measurable space; μ is any measure on X. No probability, finite measure, σ-finiteness, topology or norm on X is assumed.
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 observables.
hLfg proves Integrable L(fg) μ; hfLg proves Integrable (fLg) μ; hgLf proves Integrable (gLf) μ. Each includes a.e. strong measurability and finite norm integral.
hstationary is the single equality ∫L(fg)dμ=0. hsymmetric is the single equality ∫fLg dμ=∫gLf dμ; neither is quantified over all observables.

Mathematical proof

1. Prepare integrability for the subtraction

The first two assumptions imply integrability of L(fg)−fLg. The third integrable term gLf may then be subtracted from that difference.

\[L(fg)-fLg\in L^1(\mu).\]

Corresponding Lean step

MeasureTheory.Integrable.sub; hsub

2. Expand the Γ integral legitimately

Pull out one-half and use the two subtraction rules, whose integrability premises are now available.

\[\int_X\Gamma_L(f,g)\,d\mu=\tfrac12\left[\int_XL(fg)\,d\mu-\int_XfLg\,d\mu-\int_XgLf\,d\mu\right].\]

Corresponding Lean step

MeasureTheory.integral_const_mul; MeasureTheory.integral_sub; hgammaIntegral

3. Prove equality of the two pairings

The definition negates the two cross integrals; their assumed equality therefore gives symmetric pairings for this pair.

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

Corresponding Lean step

Generator.dirichletForm; hsymmetric

4. Use the supplied zero product integral and pairing symmetry

Set A=∫fLg dμ. The expansion becomes one-half of 0−A−A, hence equals −A, which is the Dirichlet pairing.

\[\int_X\Gamma_L(f,g)\,d\mu=\tfrac12(0-A-A)=-A=\mathcal E_\mu^L(f,g).\]

Corresponding Lean step

hstationary; hsymmetric; Generator.dirichletForm; ring

5. Collect both conclusions

The theorem returns the conjunction of pair symmetry and the integrated Γ identity, not a global property of L.

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

Corresponding Lean step

constructor

Lean statement · fundamental_integration_by_parts

There are three integrability proofs and two exact integral identities. They are explicit local hypotheses rather than an assumption that μ is a globally stationary reversible law. The conclusion contains two equalities joined by conjunction.

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.

theorem fundamental_integration_by_parts
    [MeasurableSpace X]
    (mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ)
    (hLfg : Integrable (generator (f * g)) mu)
    (hfLg : Integrable (fun x => f x * generator g x) mu)
    (hgLf : Integrable (fun x => g x * generator f x) mu)
    (hstationary : (∫ x, generator (f * g) x ∂mu) = 0)
    (hsymmetric :
      (∫ x, f x * generator g x ∂mu) =
        ∫ x, g x * generator f x ∂mu) :
    FunctionalInequalities.Generator.dirichletForm mu generator f g =
        FunctionalInequalities.Generator.dirichletForm mu generator g f ∧
      FunctionalInequalities.Generator.dirichletForm mu generator f g =
        ∫ x, carreDuChamp generator f g x ∂mu

Exact module and namespace context

Lean proof · fundamental_integration_by_parts

The proof splits the Γ integral using the three integrability inputs, substitutes the local zero-integral and symmetry equations, and simplifies real arithmetic. The same symmetry equation directly proves the first equality.

theorem fundamental_integration_by_parts
    [MeasurableSpace X]
    (mu : Measure X) (generator : (X → ℝ) →ₗ[ℝ] (X → ℝ))
    (f g : X → ℝ)
    (hLfg : Integrable (generator (f * g)) mu)
    (hfLg : Integrable (fun x => f x * generator g x) mu)
    (hgLf : Integrable (fun x => g x * generator f x) mu)
    (hstationary : (∫ x, generator (f * g) x ∂mu) = 0)
    (hsymmetric :
      (∫ x, f x * generator g x ∂mu) =
        ∫ x, g x * generator f x ∂mu) :
    FunctionalInequalities.Generator.dirichletForm mu generator f g =
        FunctionalInequalities.Generator.dirichletForm mu generator g f ∧
      FunctionalInequalities.Generator.dirichletForm mu generator f g =
        ∫ x, carreDuChamp generator f g x ∂mu := by
  have hsub : Integrable
      (fun x => generator (f * g) x - f x * generator g x) mu :=
    hLfg.sub hfLg
  have hgammaIntegral :
      (∫ x, carreDuChamp generator f g x ∂mu) =
        (2 : ℝ)⁻¹ *
          ((∫ x, generator (f * g) x ∂mu) -
            (∫ x, f x * generator g x ∂mu) -
            ∫ x, g x * generator f x ∂mu) := by
    change
      (∫ x, (2 : ℝ)⁻¹ *
        (generator (f * g) x - f x * generator g x -
          g x * generator f x) ∂mu) = _
    rw [integral_const_mul,
      integral_sub hsub hgLf, integral_sub hLfg hfLg]
  constructor
  · simp only [FunctionalInequalities.Generator.dirichletForm]
    rw [hsymmetric]
  · simp only [FunctionalInequalities.Generator.dirichletForm]
    rw [hgammaIntegral, hstationary, hsymmetric]
    ring

/-- Chewi Corollary 1.2.15: the negative reversible generator has a
nonnegative quadratic form once Gamma is pointwise nonnegative. -/

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.
The explicit integrability inputs prevent invalid linear expansion of totalized nonintegrable integrals; they must not be omitted.
This is algebraic generator integration by parts, not a spatial divergence theorem with boundary terms or a concrete gradient identity.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Integrable.sub
MeasureTheory.integral_const_mul
MeasureTheory.integral_sub

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-theorem-1-2-14 — Existing local record for Chewi Theorem1.2.14, 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.
Integrable subtraction — Produces hsub from hLfg and hfLg.
Integral subtraction with both integrability premises — Used twice to expand Γ. Constant multiplication is at288.
Exact negative-generator convention — Defines Eμ(f,g)=−∫fLg dμ.
Existing focused test — Declaration-visibility #check only; no nontrivial stationary/reversible model is constructed in this focused file. 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.