ASTIS mathematical exposition

The Euclidean space used by the Dirichlet bridge

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

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

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

abbrev State

Exact module and namespace context

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.

abbrev State := EuclideanSpace ℝ ι

/-- The canonical density/log-ratio pair is in the generator integration-by-
parts domain needed to invoke Chewi Theorem 1.2.14.

The fields are exactly the three integrability terms, stationarity of the
product observable, and generator symmetry for this pair.  This is a local
pair contract, not a global reversibility claim. -/

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.

Source and reuse

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

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