Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Extract one admissible scalar value from a known supremum

AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar · theorem · Teaching coverage

Read this first

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

\[v\in A,\quad A\text{ bounded above},\quad\sup A=k,\quad v=e-L \Longrightarrow e\le k+L.\]
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.

Download module (.lean)
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

Exact module and namespace context

Proof roadmap

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

  2. 2Substitute the supplied meanings

    Replace v by e−L and sup A by k to obtain a variational upper bound.

  3. 3Apply scalar rearrangement

    The previously established subtraction lemma gives the one-sided sum form.

Full assumptions and notation

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.

\[v\le\sup A.\]
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.

\[e-L\le k.\]
Corresponding Lean step

rw [← htest,← hsup]; htest_le_sup

3. Apply scalar rearrangement

The previously established subtraction lemma gives the one-sided sum form.

\[e\le k+L.\]
Corresponding Lean step

dvVariationalOneSidedConsequenceScalar hvar

Lean verification

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

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

Download module (.lean)
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

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.
  • The entropy supremum equality and admissible-test membership are not established here.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • le_csSup

Mathematical sources

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