The Legendre transform of Λ : ℝ → ℝ at a: Λ^*(a) := sup_λ (λ·a − Λ(λ)).

Mathlib has no general Legendre-transform / convex-conjugate API, so this is the textbook sSup form. When the image set is not BddAbove, Mathlib returns sSup = 0, so the basic properties below take an explicit BddAbove hypothesis.

Cramér rate function I(a) := Λ^*(a) for Λ := cgf X μ.

Each linear-minus-Λ value is ≤ the Legendre transform.

If Λ 0 = 0 (e.g. Λ = cgf X μ for a probability measure), the Legendre transform is non-negative whenever the supremum exists.

Cramér rate-function version of legendre_apply_le.

Cramér rate function is non-negative whenever the Legendre supremum exists for a probability measure (then cgf X μ 0 = 0).

For a bounded real random variable on a finite measure space, the exponential moment exp (t * Y) is integrable for every t. This is the hypothesis-eliminator the Cramér chain uses to remove Integrable premises from the main statements.

i.i.d. CGF sum formula: for an i.i.d. family X : ℕ → Ω → ℝ (with X i identically distributed to X 0 and the exponential moments integrable for every i), cgf (∑ i ∈ range n, X i) μ t = n · cgf (X 0) μ t.

Per-n Chernoff bound for the upper tail of an i.i.d. sum of bounded real random variables: tilting by any lam ≥ 0, the upper-tail probability decays exponentially with rate at least lam * a − Λ(lam).

Per-n Cramér upper bound, log form: for each n ≥ 1 with positive tail probability, (1/n) · log P[a·n ≤ Sₙ] ≤ -(lam · a − Λ(lam)) for every lam ≥ 0.

Cramér's theorem (upper bound, limsup form): for each lam ≥ 0, the upper-tail probability of the i.i.d. sample sum decays at exponential rate at least lam * a − Λ(lam):

limsup_n (1/n) log P[a·n ≤ Sₙ] ≤ -(lam · a − Λ(lam)).

Two technical hypotheses make the result clean:

• h_pos — the tail probability is eventually positive (e.g. when a ≤ ess sup X), so that log is finite.
• h_cobdd — the resulting log-rate sequence is cobounded below in the limsup sense. This holds whenever the sequence does not blow up to -∞, e.g. when the tail probabilities admit any sub-exponential lower bound.

Cramér's theorem (upper bound, Legendre form): if the Legendre transform of Λ = cgf (X 0) μ at a is attained by some non-negative lam (hlam_opt), then

limsup_n (1/n) log P[a·n ≤ Sₙ] ≤ -cramerRate (X 0) μ a.

hlam_opt is a regularity precondition (it holds for a ≥ 𝔼[X] by convexity of the Legendre transform), not part of the proof core.

See also cramer_upper.

Universal integrability for bounded RVs: a bounded random variable has every t ∈ ℝ in its integrableExpSet, hence the whole real line lies in the interior. This kills the interior (integrableExpSet X μ) hypothesis of integral_tilted_mul_self / variance_tilted_mul in the bounded-RV setting.

The tilted measure of a bounded random variable is a probability measure.

For a bounded random variable Y, the expectation of Y under μ.tilted (lam * Y ·) equals the first derivative of cgf Y μ at lam.

KL-of-tilted identity.

For a bounded real random variable X : Ω → ℝ on a probability measure μ, the (integral form of the) Kullback-Leibler divergence between μ.tilted (lam * X ·) and μ admits the closed form

∫ ω, log (rnDeriv (μ.tilted (lam * X ·)) μ ω).toReal ∂(μ.tilted (lam * X ·)) = lam * (μ.tilted (lam * X ·))[X] - cgf X μ lam.

We work directly with the ∫ log (rnDeriv) representation rather than the ℝ≥0∞-valued klDiv to keep the algebraic identity transparent.