Extract one admissible scalar value from a known supremum
AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar · theorem · Teaching coverage
Statement
Let A⊆ℝ be bounded above, let v∈A, and suppose sup A=k and v=e−L for real k,e,L,v. Then e≤k+L. Membership supplies nonemptiness; the supremum identity and the selected test's representation are assumptions.
All objects and hypotheses
- admissibleValues=A is a set of real numbers; hbounded says A is bounded above.
- testValue=v belongs to A; kl=k, expectation=e and logMgf=L are real.
- hsup gives sSup A=k and htest gives v=e−L.
Mathematical proof
1. Bound the selected value by the supremum
For a bounded-above real set, every member is at most its supremum. The member v makes an additional nonemptiness assumption unnecessary.
Corresponding Lean step
le_csSup hbounded hmem
2. Substitute the supplied meanings
Replace v by e−L and sup A by k to obtain a variational upper bound.
Corresponding Lean step
rw [← htest,← hsup]; htest_le_sup
3. Apply scalar rearrangement
The previously established subtraction lemma gives the one-sided sum form.
Corresponding Lean step
dvVariationalOneSidedConsequenceScalar hvar
Lean statement · dvVariationalOneSidedFromSupremumScalar
The set consists of scalar values. This theorem does not define admissible random variables or prove that its supremum is KL.
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 dvVariationalOneSidedFromSupremumScalar {admissibleValues : Set Real}
{kl expectation logMgf testValue : Real}
(hbounded : BddAbove admissibleValues)
(hmem : testValue ∈ admissibleValues)
(hsup : sSup admissibleValues = kl)
(htest : testValue = expectation - logMgf) :
expectation ≤ kl + logMgfLean proof · dvVariationalOneSidedFromSupremumScalar
The proof uses the real supremum order theorem, rewrites the two assumed identities, and reuses the scalar consequence.
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 dvVariationalOneSidedFromSupremumScalar {admissibleValues : Set Real}
{kl expectation logMgf testValue : Real}
(hbounded : BddAbove admissibleValues)
(hmem : testValue ∈ admissibleValues)
(hsup : sSup admissibleValues = kl)
(htest : testValue = expectation - logMgf) :
expectation ≤ kl + logMgf := by
have htest_le_sup : testValue ≤ sSup admissibleValues := le_csSup hbounded hmem
have hvar : expectation - logMgf ≤ kl := by
rw [← htest, ← hsup]
exact htest_le_sup
exact dvVariationalOneSidedConsequenceScalar hvar
/-- Finite-log-mgf monotonicity for the scaled tests used before DV.
If the exponential moment for `alpha0 * q` is integrable under a finite
measure, then the exponential moment for `alpha * q` is integrable for
`0 <= alpha <= alpha0`. In SALD this is the local Mathlib-backed part of
turning an `alpha0`-complexity assumption into the finite-log-mgf hypothesis
for a selected DV test; it is not a proof of the DV formula itself.
-/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.
- The entropy supremum equality and admissible-test membership are not established here.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- le_csSup
Mathematical sources
- Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
- AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar — Existing root ASTIS dependency; use its own adjacent teaching unit.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.