PhyslibAlpha.ClassicalFieldTheory.Local.Variation

Alpha extensions for admissible local variations

i. Overview

This module adds the Euclidean component API needed by the coordinate-readout CFT stack in `PhyslibAlpha`.

The underlying `AdmissibleVariation` structure remains the maintained one from `Physlib`; this file only adds helper lemmas used by the Alpha development.

ii. Key results

`ClassicalFieldTheory.Local.AdmissibleVariation.coord_euclidean`

1 declaration

theorem

The Euclidean components of an admissible variation are test functions

#coord_euclidean

Let $\eta$ be an admissible local variation on a space of dimension $d$ with values in the Euclidean space $\mathbb{R}^m$ . For any coordinate index $a \in \{0, \dots, m-1\}$ , the scalar-valued function mapping $x$ to the $a$ -th component of $\eta(x)$ , denoted by $x \mapsto (\eta(x))_a$ , is a test function.