Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

The shared finite-dimensional Euclidean state space

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

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

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

abbrev State

Exact module and namespace context

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.

abbrev State := EuclideanSpace ℝ ι

/-- Pointwise relative-Fisher energy for a supplied density and a supplied
log-density ratio. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No probability, positivity-of-dimension, or infinite-dimensional Fisher theorem is asserted.

Source and reuse

ASTIS parents called

    Mathlib API called (external library)

    • EuclideanSpace

    Mathematical sources

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