Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Jensen's inequality for an integrable cost random variable

Statement

Let a∈R, let f:[a,∞)→R be finite and concave, and let U be an integrable real random variable with U≥a almost surely and f(U) integrable. Then Ef(U)≤f(EU).

Facts & Assumptions

Given: A real number a, a finite concave function f on [a,∞), and an integrable random variable U≥a for which f(U) is integrable.

[A1]

The domain, concavity, integrability, and lower-bound hypotheses in the Statement.

[F1]

Dedekind completeness: the least-upper-bound property: every nonempty subset of R bounded above has a real supremum.

[F2]

A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere: on any measure space, a nonnegative measurable function has integral zero exactly when it is zero almost everywhere.

Proof

1.1A1F2givenalgebracases

Put m=EU≥a. If m=a, let V=(U−a)+, a nonnegative measurable variable equal to U−a almost surely by [A1]. Thus EV=EU−a=0. Applying [F2] with the probability measure gives V=0 almost surely; combined with U≥a almost surely this implies U=a almost surely. Consequently Ef(U)=f(a)=f(m).

1.2A1F1givenalgebra

Suppose m>a. For y>m define r(y)=(f(y)−f(m))/(y−m). Concavity applied to a<m<y gives r(y)≤(f(m)−f(a))/(m−a), and the right-slope set is nonempty (take y=m+1) and bounded above; [F1] supplies its finite supremum s. For each x with a≤x<m and each y>m, concavity at x<m<y gives (f(m)−f(x))/(m−x)≥r(y); taking the supremum over y yields (f(m)−f(x))/(m−x)≥s. Therefore every u≥a satisfies f(u)≤f(m)+s(u−m).

2.1A1step 1.1step 1.2algebracases∎

The affine upper bound in step 1.2 is integrable because U is integrable. Taking expectations gives Ef(U)≤f(m)+s(EU−m)=f(m). Together with step 1.1 this proves the claim.

Depends on

Used by

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources