Sobolev witnesses

This file is the DGM-style Sobolev witness layer. It bundles a map together with the displayed weak gradient and the local W^{1,2} data needed by the monotonicity proof.

No stationarity or monotonicity theorem is defined here; those live in StationaryMap.lean and MainTheorem.lean.

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

A local W^{1,2} witness for a map, carrying the chosen weak gradient.

This is intentionally a Type, not a Prop: the weak gradient is data that the public monotonicity theorem must use in the monotonicity quantity.

• weakGrad : Domain n → Gradient n m

  The displayed weak gradient.

• map_memLpTwo_loc : LocallyMemLpTwoIn u Omega

  Local L^2 control of the map.

• grad_aestronglyMeasurable : GradientAEStronglyMeasurableIn self.weakGrad Omega

  A.e. strong measurability of the displayed weak gradient.

• grad_memLpTwo_loc : LocallyMemLpTwoIn self.weakGrad Omega

  Local L^2 control of the displayed weak gradient.

• isWeakGradient : DistributionalWeakGradientIn u self.weakGrad Omega

  The displayed gradient is the distributional weak gradient of the map.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocMapWitness.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) : W12LocMapWitness u Omega

Build a local Sobolev witness from its component hypotheses.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocMapWitness.toSobolevW12LocIn {n m : ℕ} {u : Domain n → Target m} {Omega : Set (Domain n)} (h : W12LocMapWitness u Omega) : SobolevW12LocIn u h.weakGrad Omega

Forget the explicit witness package to the earlier Sobolev bridge.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocMapWitness.toW12LocIn {n m : ℕ} {u : Domain n → Target m} {Omega : Set (Domain n)} (h : W12LocMapWitness u Omega) : W12LocIn u h.weakGrad Omega

Forget the explicit witness package to the custom weak W^{1,2}_{loc} interface used internally by the monotonicity proof.