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

The shared finite-dimensional Euclidean state space

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RelativeFisher.State · abbrev · Teaching coverage

Read this first

Mathematical statement

State is the local name for Mathlib's real Euclidean space indexed by ι. The abbreviation itself can be formed for any index type; subsequent energy and gradient declarations in this module assume ι finite.

\[E:=\operatorname{EuclideanSpace}(\mathbb R,\iota).\]
Lean statement · State

This is a shorter type name, not a theorem about a state space or a probability distribution.

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)
abbrev State

Exact module and namespace context

Proof roadmap

  1. 1Reuse the existing coordinate space

    The local name unfolds directly to Mathlib's Euclidean type; no geometric structure is constructed anew.

Full assumptions and notation

All objects and hypotheses

  • ι is an index type. No Fintype proof is used by the abbreviation itself; finite-dimensional analysis later uses the surrounding Fintype ι instance.
  • No measure, function, or positive-dimension assumption.

Construction and meaning

1. Reuse the existing coordinate space

The local name unfolds directly to Mathlib's Euclidean type; no geometric structure is constructed anew.

\[\mathrm{State}\equiv\operatorname{EuclideanSpace}(\mathbb R,\iota).\]
Corresponding Lean step

EuclideanSpace

Lean verification

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

Lean construction · State

There is no proof. The abbreviation expands to the existing Mathlib coordinate type.

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)
abbrev State := EuclideanSpace ℝ ι

Exact module and namespace context

Scope and omitted-condition boundaries
  • No probability, positivity-of-dimension, or infinite-dimensional Fisher theorem is asserted.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

    Mathlib API called (external library)

    • EuclideanSpace

    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.