Documentation

HighDimProb.Analysis.RealInequalities

Real inequalities for moment growth #

Verified Wikipedia references:

Note: real-analysis background is available at https://en.wikipedia.org/wiki/Real_analysis, but the formulas below are specifically exponential/Gaussian-tail envelope inequalities.

This file contains small deterministic real-analysis helpers used by the concentration moment layer. It deliberately avoids probability assumptions.

source
theorem HighDimProb.exp_mul_le_chord_exp_of_nonneg_of_le {c x sigma : ℝ} (_hc : 0 ≤ c) (hx0 : 0 ≤ x) (hxsigma : x ≤ sigma) (hsigma : 0 < sigma) :
Real.exp (c * x) ≤ 1 + x / sigma * (Real.exp (c * sigma) - 1)

Scalar exponential chord bound on [0, sigma].

This is the one-dimensional convexity helper used before matrix/eigenvalue bookkeeping: it keeps the downstream 0 <= c assumption in the signature even though convexity of exp proves the inequality for arbitrary c.

source
theorem HighDimProb.log_le_sq_of_nonneg {y : ℝ} (hy : 0 ≤ y) :
Real.log y ≤ y ^ 2

A convenient elementary bound used to dominate powers by Gaussian tails.

source
theorem HighDimProb.pow_le_exp_nat_mul_sq {y : ℝ} (hy : 0 ≤ y) (q : ℕ) :
y ^ q ≤ Real.exp (↑q * y ^ 2)

Powers are dominated by a Gaussian exponential envelope.

source
theorem HighDimProb.pow_le_two_sqrt_mul_exp_sq {x : ℝ} (hx : 0 ≤ x) {q : ℕ} (hq : 1 ≤ q) :
x ^ q ≤ (2 * √↑q) ^ q * Real.exp (x ^ 2 / 4)

Deterministic sharp-growth envelope for natural powers.

The constant 2 is the main helper; a constant-4 compatibility wrapper is provided below for theorem statements that use a looser envelope.

source
theorem HighDimProb.pow_le_two_mul_scale_sqrt_mul_exp_sq_div_four {x K : ℝ} (hx : 0 ≤ x) (hK : 0 < K) {q : ℕ} (hq : 1 ≤ q) :
x ^ q ≤ (2 * K * √↑q) ^ q * Real.exp ((x / K) ^ 2 / 4)

Scaled version of pow_le_two_sqrt_mul_exp_sq.

source
theorem HighDimProb.pow_le_two_mul_scale_sqrt_mul_exp_sq_div {x K : ℝ} (hx : 0 ≤ x) (hK : 0 < K) {q : ℕ} (hq : 1 ≤ q) :
x ^ q ≤ (2 * K * √↑q) ^ q * Real.exp ((x / K) ^ 2)

A looser scaled envelope with the full exponential-square term.

source
theorem HighDimProb.two_mul_pow_le_two_mul_pow {a : ℝ} (ha : 0 ≤ a) {q : ℕ} (hq : 1 ≤ q) :
2 * a ^ q ≤ (2 * a) ^ q

Absorb a leading factor 2 by doubling the base of a nonzero natural power.

source
theorem HighDimProb.pow_le_four_sqrt_mul_exp_sq {x : ℝ} (hx : 0 ≤ x) {q : ℕ} (hq : 1 ≤ q) :
x ^ q ≤ (4 * √↑q) ^ q * Real.exp (x ^ 2 / 4)

Constant-4 compatibility wrapper for the deterministic envelope.

Bounded scalar Bernstein exponential inequality #

The deterministic scalar inequality behind the matrix Bernstein functional-calculus step. It is purely real analysis and carries no probability or matrix content.

source
theorem HighDimProb.exp_le_one_add_add_half_sq_div_one_sub_third {u b : ℝ} (hub : |u| ≤ b) (hb : b < 3) :
Real.exp u ≤ 1 + u + u ^ 2 / 2 / (1 - b / 3)

Bounded scalar Bernstein exponential inequality.

For a real number u with |u| ≤ b and b < 3, exp u ≤ 1 + u + (u ^ 2 / 2) / (1 - b / 3).

The constant (1 / 2) / (1 - b / 3) is the canonical bounded-Bernstein moment-generating-function coefficient.