Mathlib.Analysis

Bernoulli KL Band Bound

This file proves a scalar upper bound on the Kullback--Leibler divergence between two Bernoulli laws whose success probabilities both lie in the interval $[1/4,3/4]$. It supplies a Mathlib-adjacent analytic estimate used by finite-sample information arguments elsewhere in the library.

Clipping a real number into a closed interval

Truncating (clipping, clamping, winsorising) a real number to a closed interval [a, b] is ubiquitous in estimation: propensity scores are clipped away from 0 and 1, outcomes and privatised statistics are clipped to a symmetric band [-B, B], and so on. Every such argument needs the same four facts — the clipped value lies in the interval, values already inside are untouched, the map is 1-Lipschitz, and clipping never increases the distance (nor the squared distance) to any target that is itself inside the interval.

Mathlib proves the contraction property, but only for the subtype-valued projection Set.projIcc : ℝ → Set.Icc a b, which is awkward to use when the surrounding development works with plain reals. This file provides the real-valued companion clipIcc a b x = max a (min b x) (definitionally the underlying value of Set.projIcc) together with the facts above, so that a symmetric band [-B, B], an asymmetric propensity band [q, 1 - q], and either the max-outside or the min-outside spelling are all instances of one API.

Projection onto closed convex sets

This module provides metric projection onto a nonempty closed convex subset of a real Hilbert space, together with its variational, contraction, continuity, and measurability properties. It also specializes the construction to a Loewner interval of real matrices, using Frobenius distance, and supplies the associated matrix inequalities.

Fréchet's functional equation (degree-one case)

Fréchet-style finite-difference arguments appear in classical proofs of independence characterization theorems. This file proves the foundational degree-one case: a continuous function with vanishing second forward difference is affine (affine_of_continuous_of_second_diff_zero).

The argument is classical: a vanishing second difference makes f midpoint-affine; subtracting f 0 yields an additive function; a continuous additive map of real vector spaces is ℝ-linear (AddMonoidHom.toRealLinearMap).

Coordinates of a Euclidean gradient as directional derivatives

A single bridge lemma: the a-th coordinate of the (Riesz) gradient of a real-valued function on a finite-dimensional Euclidean space equals the ordinary one-variable derivative of the function along the a-th coordinate line. This is the standard tool for computing a gradient coordinate by coordinate — reduce each entry to a deriv of a one-parameter restriction, which the univariate calculus API can then evaluate.

Polar integration and cancellation on half-discs

This module derives weighted polar-integration formulas on upper half-discs, including radial mass identities, odd-angular cancellation, quadratic angular moments, and translation-invariant variants.

Second directional derivative along an affine line

For f : E → ℝ and a direction d : E, the restriction of f to the line s ↦ f (q + s • d) has first and second derivatives expressible as directional derivatives of f at the moving base point q + t • d:

* deriv_line : deriv (fun s => f (q + s • d)) t = fderiv ℝ f (q + t • d) d * deriv_deriv_line: `deriv (deriv fun s => f (q + s • d)) t = secondDirDeriv f d (q + t • d)`

where secondDirDeriv f d q = fderiv ℝ (fun x => fderiv ℝ f x d) q d. Two consequences make secondDirDeriv usable as a curvature modulus over a constraint set:

* continuous_secondDirDeriv : it is continuous in the base point (so it is bounded on a compact set, giving the BddAbove needed for a ciSup), and * convexOn_deriv2_nonneg : a convex C² function of one variable has nonnegative second derivative at interior points (so such a modulus is nonnegative).

Mathlib has convexOn_of_deriv2_nonneg (sufficiency) but not the converse used here.

The statements are objective-agnostic: callers supply ContDiff ℝ 2 f and read off the directional curvature. This is the substrate behind the dirModulus / EnvelopeLineC2Data discharge for the reciprocal-product variance envelope.

Multivariate monomial Gram matrices

This module proves that distinct multivariate monomials have a positive-definite Gram matrix on every nondegenerate real cube. It also supplies the resulting uniform quadratic coercivity bound.

Offset peeling inequalities

This file gives deterministic Young/weighted-AM-GM bounds that control expressions of the form a·t^θ after subtracting a linear offset in t. It provides the quarter-offset constant offsetPeelingConstant, its general coefficient version offsetPeelingConstantC, the corresponding peeling bounds offset_peeling and offset_peeling_coeff, endpoint extensions at θ = 0, and max_two_split for splitting a clipped two-term offset across summands.

Small real-power arithmetic helpers

This file provides reusable arithmetic identities and inequalities for real powers and square roots, especially for sample-size factors and negative exponents. The main lemmas identify reciprocals with real powers (inv_eq_rpow_neg_one), factor (A / n) ^ p into an A part and an n part (div_rpow_of_nonneg_of_pos), bound nonpositive powers of natural casts (rpow_natCast_nonpos_le_one), and rewrite q⁻¹ * sqrt q as q ^ (-1/2) (inv_mul_sqrt_eq_rpow_neg_half).

Second-order descent for one real variable

This module provides the one-dimensional smooth-optimization descent lemma. A real function whose second derivative is bounded above in a segment's interior lies below the corresponding quadratic Taylor model, and a negative initial slope gives an explicit positive decrease at the clipped quadratic-model step.

The statements are objective-agnostic. Callers supply the regularity on Set.Icc 0 T and the interior pointwise second-derivative bound; this file only turns those hypotheses into the quadratic upper bound and the optimized descent gap.

A globally C¹ reciprocal with a floor near the singularity

The reciprocal x ↦ x⁻¹ is singular at 0. recipC ε is a modification that agrees with x⁻¹ on x ≥ ε/2 but is smoothly damped to 0 on the neighbourhood of the singularity, so it is globally C¹ on all of ℝ. This is the reusable core of the "globally C¹ extension of an objective that is singular on the boundary of its feasible box" pattern: multiply the singular part by a Real.smoothTransition cutoff that is 1 on the feasible region and 0 past the boundary.

Cauchy–Schwarz against a finite nonnegative weight vector

Mathlib's discrete Cauchy–Schwarz Finset.sum_mul_sq_le_sq_mul_sq is stated for the unweighted inner product. Weighted versions (⟨f, g⟩_w = Σ wᵢ fᵢ gᵢ for a nonnegative weight vector w) get re-derived by hand all over the library, so this module records them once, over an arbitrary finite support.

* weighted_inner_sq_le — squared form (Σ wᵢ fᵢ gᵢ)² ≤ (Σ wᵢ fᵢ²)(Σ wᵢ gᵢ²). * abs_weighted_inner_le — square-root form with an absolute value on the left. * abs_weighted_mean_le_sqrt_weighted_sq — the subprobability-weight (Σ wᵢ ≤ 1) specialization |Σ wᵢ fᵢ| ≤ √(Σ wᵢ fᵢ²), i.e. Jensen for x ↦ x². * weighted_sqrt_le_sqrt_weighted — Jensen for √·: Σ wᵢ √qᵢ ≤ √(Σ wᵢ qᵢ).

All four follow from the unweighted inequality by substituting f ↦ √w · f, g ↦ √w · g and simplifying with Real.sq_sqrt.