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.Mathematics.VariationalCalculus.IsTestFunctionAdmissible local variations
i. Overview
This module packages the admissible variations used in the local first-variation problem.
For the first local stage, a variation is admissible if it is a smooth compactly supported map
Space d → U for a real normed vector space U. This reuses the existing IsTestFunction
predicate rather than introducing a second support calculus.
ii. Key results
ClassicalFieldTheory.Local.AdmissibleVariation : compactly supported smooth variations.
iii. Table of contents
A. Admissible variations
B. Basic operations on admissible variations
iv. References
@[expose] public sectionA. Admissible variations
An admissible local variation is a smooth compactly supported map Space d → U.
The underlying variation function.
Smoothness and compact support of the variation.
structure AdmissibleVariation (d : ℕ) (U : Type*) [NormedAddCommGroup U] [NormedSpace ℝ U] where toFun : Space d → U isTestFunction : IsTestFunction toFunB. Basic operations on admissible variations
instance : CoeFun (AdmissibleVariation d U) (fun _ => Space d → U) where
coe η := η.toFunattribute [fun_prop] AdmissibleVariation.isTestFunctionAn admissible variation has compact support.
lemma hasCompactSupport (η : AdmissibleVariation d U) : HasCompactSupport (η.toFun) :=
η.isTestFunction.supp@[simp]
lemma zero_apply (x : Space d) : (0 : AdmissibleVariation d U) x = 0 := rfl@[simp]
lemma neg_apply (η : AdmissibleVariation d U) (x : Space d) : (-η) x = -η x := rfl@[simp]
lemma add_apply (η ξ : AdmissibleVariation d U) (x : Space d) : (η + ξ) x = η x + ξ x := rfl@[simp]
lemma sub_apply (η ξ : AdmissibleVariation d U) (x : Space d) : (η - ξ) x = η x - ξ x := rfl@[simp]
lemma smul_apply (c : ℝ) (η : AdmissibleVariation d U) (x : Space d) :
(c • η) x = c • η x := rfl@[fun_prop]
lemma coord {m : ℕ} (η : AdmissibleVariation d (Space m)) (a : Fin m) :
IsTestFunction (fun x => (η.toFun x).coord a) := d:ℕm:ℕη:AdmissibleVariation d (Space m)a:Fin m⊢ IsTestFunction fun x => Space.coord a (η.toFun x)
All goals completed! 🐙