PhyslibAlpha.ClassicalFieldTheory.Local.Variation

Imports

/-
Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Juan Jose Fernandez Morales
-/
module

public import Physlib.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

@[expose] public section

A Euclidean component of an admissible variation is again a test function.

@[fun_prop]
lemma coord_euclidean (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (a : Fin m) :
    IsTestFunction (fun x => (η.toFun x) a) := byd:ℕm:ℕη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))a:Fin m⊢ IsTestFunction fun x => (η.toFun x).ofLp a
  exact η.isTestFunction.comp_left (g := fun v : EuclideanSpace ℝ (Fin m) => v a)
    (byd:ℕm:ℕη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))a:Fin m⊢ WithLp.ofLp 0 a = 0 simpAll goals completed! 🐙) (byd:ℕm:ℕη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))a:Fin m⊢ ContDiff ℝ ↑⊤ fun v => v.ofLp a fun_propAll goals completed! 🐙)