Samplinglib mathematical lesson

The PiLp equivalence preserves coordinate vectors

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.continuousLinearEquiv_apply_euclideanSpace_single · theorem · Teaching coverage

Read this first

Mathematical statement

For a finite coordinate type ι and any i∈ι, the canonical equivalence from Euclidean coordinates to the raw function space sends the Euclidean i-th unit vector to the raw i-th unit function.

\[e(\operatorname{EuclideanSingle}(i,1))=\operatorname{PiSingle}(i,1).\]

Lean statement · continuousLinearEquiv_apply_euclideanSpace_single

The equivalence preserves coordinates, but it is not asserted to preserve the supremum and ℓ² norms.

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)

theorem continuousLinearEquiv_apply_euclideanSpace_single
    {ι : Type*} [Fintype ι] [DecidableEq ι] (i : ι) :
    (PiLp.continuousLinearEquiv 2 ℝ (fun _ : ι => ℝ))
      (EuclideanSpace.single i (1 : ℝ)) = Pi.single i (1 : ℝ)

Exact module and namespace context

Proof roadmap

1Compare every coordinate
At coordinate j both vectors have value one when j=i and zero otherwise. Extensional equality of functions proves the asserted vector equality.

Full assumptions and notation

All objects and hypotheses

ι is a finite type with chosen finite enumeration and decidable equality; V=EuclideanSpace ℝ ι carries the Euclidean ℓ² norm. Empty ι is allowed.
e:V≃L[ℝ](ι→ℝ) is PiLp.continuousLinearEquiv 2 ℝ (fun _=>ℝ); i∈ι.

Mathematical proof

1. Compare every coordinate

At coordinate j both vectors have value one when j=i and zero otherwise. Extensional equality of functions proves the asserted vector equality.

\[\bigl(e(e_i^V)\bigr)_j=\begin{cases}1,&j=i,\\0,&j\ne i,\end{cases}=(e_i^P)_j.\]

Corresponding Lean step

ext j; PiLp.continuousLinearEquiv_apply; EuclideanSpace.single; case split j = i and simplification of Pi.single.

Lean verification

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

Lean proof · continuousLinearEquiv_apply_euclideanSpace_single

At coordinate j both vectors have value one when j=i and zero otherwise. Extensional equality of functions proves the asserted vector equality. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

Download module (.lean)

theorem continuousLinearEquiv_apply_euclideanSpace_single
    {ι : Type*} [Fintype ι] [DecidableEq ι] (i : ι) :
    (PiLp.continuousLinearEquiv 2 ℝ (fun _ : ι => ℝ))
      (EuclideanSpace.single i (1 : ℝ)) = Pi.single i (1 : ℝ) := by
  ext j
  rw [PiLp.continuousLinearEquiv_apply]
  simp [EuclideanSpace.single]
  by_cases h : j = i
  · subst h
    simp [Pi.single]
  · simp [Pi.single, h]

Exact module and namespace context

Scope and omitted-condition boundaries

No isometry or change-of-variables-integration claim.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

PiLp.continuousLinearEquiv_apply
EuclideanSpace.single
Pi.single

Mathematical sources

Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
Existing curated module card — Existing declaration-specific attribution entry, read as documentation without a new source-equivalence verdict.
Existing focused test — Exact named declaration invocation located in an existing example; no test was run.

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