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

The Euclidean state-space name

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

Read this first

Mathematical statement

For an index type ι, State is simply the existing Mathlib Euclidean space of real ι-indexed coordinates. The abbreviation itself imposes no finiteness proof; the surrounding Fisher development assumes ι is finite when using the usual Euclidean calculus.

\[E:=\operatorname{EuclideanSpace}(\mathbb R,\iota);\qquad\text{for finite }\iota,\quad \langle x,y\rangle=\sum_{i\in\iota}x_i y_i,\quad\|x\|^2=\sum_{i\in\iota}x_i^2.\]
Lean statement · State

This line introduces a shorter name for the existing coordinate space. The index type specifies its coordinate labels; it is not a theorem asserting an analytic fact about that space.

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 space

    Give Mathlib's EuclideanSpace ℝ ι the local short name State; no elements, norms, or topology are reconstructed.

Full assumptions and notation

All objects and hypotheses

  • ι is an arbitrary index type for the abbreviation itself. In the surrounding section, Fintype ι is available for subsequent finite-dimensional analysis.
  • No measure, density, gradient, probability assumption, or Nonempty ι proof is needed to name State.

Construction and meaning

1. Reuse the existing space

Give Mathlib's EuclideanSpace ℝ ι the local short name State; no elements, norms, or topology are reconstructed.

\[\mathrm{State}=\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 to supply. The right-hand expression is the underlying Mathlib type, so Lean can unfold the abbreviation whenever a later definition needs Euclidean calculus.

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
  • The module's later declarations work with finite ι. This abbreviation does not create an independent state-space construction or an infinite-dimensional Fisher theorem.
  • No positivity-of-dimension or probability-law assumption.
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.