Stationary Sobolev map package

This file adds stationarity to the Sobolev witness layer. The package is the paper-facing input for the monotonicity theorem: a local Sobolev map with an explicit weak gradient, plus vanishing domain first variation.

The target-manifold constraint is intentionally absent. The monotonicity proof uses only this stationary package.

structure LeanStationaryHarmonicMaps.StationaryHarmonicMap.StationaryW12LocMap {n m : ℕ} (u : Domain n → Target m) (Omega : Set (Domain n)) : Type

A stationary local W^{1,2} map witness.

The stationarity field is exactly the domain-variation first-variation identity. No target-manifold structure is used by the monotonicity proof.

• w12 : W12LocMapWitness u Omega

  Sobolev data together with the displayed weak gradient.

• stationary : DomainVariationStationaryIn u self.w12.weakGrad Omega

  Vanishing domain first variation for the displayed weak gradient.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.StationaryW12LocMap.ofComponents {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Omega : Set (Domain n)} (hu_memLp : LocallyMemLpTwoIn u Omega) (hDu_aesm : GradientAEStronglyMeasurableIn Du Omega) (hDu_memLp : LocallyMemLpTwoIn Du Omega) (hweakGradient : DistributionalWeakGradientIn u Du Omega) (hfirstVariation : DomainVariationStationaryIn u Du Omega) : StationaryW12LocMap u Omega

Build a stationary Sobolev witness from component hypotheses.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.StationaryW12LocMap.toStationarySobolevMapIn {n m : ℕ} {u : Domain n → Target m} {Omega : Set (Domain n)} (h : StationaryW12LocMap u Omega) : StationarySobolevMapIn u h.w12.weakGrad Omega

Forget the witness package to the earlier paper-facing stationary Sobolev package.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.StationaryW12LocMap.toWeakStationaryMapIn {n m : ℕ} {u : Domain n → Target m} {Omega : Set (Domain n)} (h : StationaryW12LocMap u Omega) : WeakStationaryMapIn u h.w12.weakGrad Omega

Forget the witness package to the custom weak stationary map interface used inside the proof.