Proof of Theorem 6, p. 34 — −log(1 − t) ≤ t + 2t² for |t| ≤ 1/2

Proved

EmpiricalDRO.Consistency.neg_log_one_sub_le

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-inequalitylogarithmp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For every real $t$ with $|t|\le 1/2$ ,

-\log(1-t)\le t+2t^2 .

In the proof of Theorem 6 (and hence of Theorem 3) this inequality, applied with $t=\tilde h(x;\xi_i)/\lambda_n$ , turns the dual objective (76) into the explicit upper bound (77).

Preamble

import Mathlib
import Definitions.Def_EmpiricalDRO_Consistency_Setting

open MeasureTheory ProbabilityTheory Filter Topology

Formal statement

namespace EmpiricalDRO.Consistency

/-- The elementary inequality used in the proof of Theorem 6, Lam, arXiv:1605.09349v1, p. 34:
`−log(1 − t) ≤ t + 2t²` for every `|t| ≤ 1/2`. -/
theorem neg_log_one_sub_le : ∀ t : ℝ, |t| ≤ 1 / 2 → -Real.log (1 - t) ≤ t + 2 * t ^ 2 := by sorry

end EmpiricalDRO.Consistency

Source

Lam, Recovering Best Statistical Guarantees via the Empirical DRO, arXiv:1605.09349v1, p. 34, proof of Theorem 6, the sentence before (77)

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph