Samplinglib mathematical lesson

The Euclidean space used by the Dirichlet bridge

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

Read this first

Mathematical statement

For an index type ι, the local name State denotes Mathlib's EuclideanSpace ℝ ι. It is definitionally the same underlying Euclidean type used in the canonical relative-Fisher module; the two namespace-local abbreviations do not create different mathematical spaces. Subsequent analysis in this module is carried out for finite ι.

\[E:=\operatorname{EuclideanSpace}(\mathbb R,\iota),\qquad\mathrm{CanonicalDirichletFisher.State}=\mathrm{CanonicalRelativeFisher.State}=E.\]

Lean statement · State

This declaration is a short name for the coordinate type used by every later density, gradient, and generator in this module. It does not attach a particular measure or choose a dynamics.

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

1Reuse the Mathlib coordinate space
The local type name unfolds directly to the existing real Euclidean space. Equality of the two local names is definitional, not a constructed transport map between spaces.

Full assumptions and notation

All objects and hypotheses

ι is any index type for the abbreviation itself; the surrounding section supplies Fintype ι to subsequent finite-dimensional analytic declarations.
No measure or generator is an input to this abbreviation. No Nonempty ι hypothesis is present.

Construction and meaning

1. Reuse the Mathlib coordinate space

The local type name unfolds directly to the existing real Euclidean space. Equality of the two local names is definitional, not a constructed transport map between spaces.

\[\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 body: the abbreviation simply expands to Mathlib's type. The inherited finite-dimensional structure is available later because the module works under the finite-index assumption.

Download module (.lean)

abbrev State := EuclideanSpace ℝ ι

Exact module and namespace context

Scope and omitted-condition boundaries

This is a namespace-local alias, not a new geometric construction or theorem about changing spaces.
No probability normalization, measure invariance, or generator property.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

EuclideanSpace

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Mathlib EuclideanSpace abbreviation — The same underlying type as the relative-Fisher module's State; no nontrivial equivalence is asserted.

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