First-variation bridge

This module gives the domain-variation stationarity identity a paper-facing name. The integrand is the current weak-gradient stress-energy integrand; the map u is included in the package parameters so the statement reads like a stationary Sobolev map hypothesis, even though the formula only depends on Du. Vector-field variations use the same bundled compactly supported C¹ test-function interface as the distributional weak-gradient bridge.

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.DomainVariationStationaryIn {n m : ℕ} (u : Domain n → Target m) (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

Vanishing domain-variation first variation for a Sobolev map with chosen weak gradient.

• firstVariation_zero (X : CompactlySupportedC1In Ω (Domain n)) : ∫ (x : Domain n) in Ω, weakStationarityIntegrand Du X.toFun x = 0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.DomainVariationStationaryIn.toWeakStationaryIn {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : DomainVariationStationaryIn u Du Ω) : WeakStationaryIn Du Ω

Domain-variation stationarity implies the custom weak stationarity interface used by the monotonicity proof.