ASTIS mathematical exposition

Rearrange a supplied variational upper bound

AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar · theorem · Teaching coverage

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.\]

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 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.

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

Exact module and namespace context

Lean proof · dvVariationalOneSidedConsequenceScalar

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

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

/-- Scalar supremum step behind the one-sided use of the cited DV formula.

This does not prove Donsker--Varadhan.  It starts after a cited or eventually
formalized theorem has identified `kl` with the supremum of the admissible
variational values, and after the selected test has been shown admissible.
-/

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.

Source and reuse

ASTIS 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.

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