Nonnegative Γ gives a nonnegative quadratic generator pairing

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

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.

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

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

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

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.