ASTIS mathematical exposition

The squared-centering integral called variance

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

Statement

For any measure μ on a measurable space E and any function f:E→ℝ, define m=∫f dμ and variance μ f=∫(f−m)² dμ. The definition does not normalize μ. It represents the usual probability variance only when the relevant probability and integrability conditions are supplied.

\[m_\mu(f):=\int_E f\,d\mu,\qquad\operatorname{Var}_\mu(f):=\int_E\big(f(x)-m_\mu(f)\big)^2\,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.
f:E→ℝ is arbitrary. No probability, finite-total-mass, integrability, or square-integrability premise; no operator is an input.

Construction and meaning

1. Choose the displayed center

The center is the integral itself, not that integral divided by μ(E). It is a real-valued expression under the totalized convention.

\[m:=\int_Ef\,d\mu.\]

Corresponding Lean step

MeasureTheory.integral

2. Integrate the squared displacement from that center

Subtract the same scalar m at every point, square, and integrate under μ.

\[\operatorname{Var}_\mu(f)=\int_E(f-m)^2\,d\mu.\]

Corresponding Lean step

Generator.variance

Lean statement · variance

The declaration accepts an arbitrary measure. Its displayed center has no mass-normalization factor, so probability-language interpretation must not be applied automatically.

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 variance (mu : Measure E) (f : E → ℝ) : ℝ

Exact module and namespace context

Lean construction · variance

There is no theorem proof: form the inner integral, then form and integrate the centered square. Both integrals are totalized unless their integrability is known.

noncomputable def variance (mu : Measure E) (f : E → ℝ) : ℝ :=
  ∫ x, (f x - ∫ y, f y ∂mu) ^ 2 ∂mu

/-- Domain conditions needed to read both sides of the generator Poincare
inequality as genuine finite integrals. -/

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.
For general μ this is not automatically the variance of the normalized law μ/μ(E). No normalization or finite-variance theorem is asserted.

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.

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