Samplinglib mathematical lesson

Rearrange a supplied variational upper bound

AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar · theorem · Teaching coverage

Read this first

Mathematical statement

For arbitrary real numbers k,e,L, if e−L≤k, then e≤k+L. The names KL, expectation and log-mgf used in the Lean declaration are labels for these real inputs, not analytic definitions.

\[e-L\le k\Longrightarrow e\le k+L.\]

Lean statement · dvVariationalOneSidedConsequenceScalar

This theorem has no measures or integrals. Its only premise is a real inequality supplied by another argument.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem dvVariationalOneSidedConsequenceScalar {kl expectation logMgf : Real}
    (hvar : expectation - logMgf ≤ kl) :
    expectation ≤ kl + logMgf

Exact module and namespace context

Proof roadmap

1Add the same real number to both sides
The ordered-field subtraction equivalence moves −L from the left to +L on the right.

Full assumptions and notation

All objects and hypotheses

kl, expectation and logMgf are arbitrary real numbers; hvar supplies expectation−logMgf≤kl.

Mathematical proof

1. Add the same real number to both sides

The ordered-field subtraction equivalence moves −L from the left to +L on the right.

\[e-L\le k\iff e\le k+L.\]

Corresponding Lean step

sub_le_iff_le_add.mp hvar

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · dvVariationalOneSidedConsequenceScalar

The proof applies a basic ordered-additive equivalence. It neither proves entropy duality nor checks an admissible test.

Download module (.lean)

theorem dvVariationalOneSidedConsequenceScalar {kl expectation logMgf : Real}
    (hvar : expectation - logMgf ≤ kl) :
    expectation ≤ kl + logMgf := by
  exact sub_le_iff_le_add.mp hvar

Exact module and namespace context

Scope and omitted-condition boundaries

Only a one-sided bound for a selected admissible test is established. The full Donsker–Varadhan/Boucheron variational supremum equality remains separate; no source-fidelity verdict is made.
Pure scalar rearrangement; analytic meanings must be supplied downstream.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

sub_le_iff_le_add

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.