Integrability Under Affine Subtraction

This states that affine subtraction preserves potential integrability under a first-moment hypothesis.

Let $\mu$ be a finite measure on a real inner-product space, let $f:E\to\overline{\mathbb R}$ be potential-integrable with respect to $\mu$, and let $a\in E$, $b\in\mathbb R$. Assume the identity map is integrable:

Then affineSubtract f a b is also potential-integrable with respect to $\mu$. No Borel-space instance is required by the statement, and no supporting affine plane is assumed.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.MomentMeasure. Shown in its original module context. Proof omitted.

theorem affineSubtract_potentialIntegrable
    (f : E → EReal) (a : E) (b : ℝ) (hf : PotentialIntegrable f μ)
    (hfirst : Integrable (fun x : E => x) μ) :
    PotentialIntegrable (affineSubtract f a b) μ

Module navigation

Module: Probability/MomentMeasure/Affine.

Definition modules: Analysis/Convex/Affine, Probability/MomentMeasure/Basic.

Next: integral_affineSubtract.

Source excerpt, lines 70–73 · Frozen source 408915f.