ASTIS mathematical exposition

The PiLp equivalence preserves coordinate vectors

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

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

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

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

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.

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]

/-- The derivative of the Euclidean radial cutoff transports to raw finite Pi
space through `WithLp.toLp 2` by the chain rule.

This is the cutoff-side `HasFDerivAt` producer consumed by the finite-box
cutoff-smul route.  It is pointwise and proves no support containment,
integrability, tail limit, or integration-by-parts identity. -/

Exact module and namespace context

Scope and omitted-condition boundaries

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

Source and reuse

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

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