Public API for stationary Sobolev map monotonicity

This module is the intended public entry point for the stationary W^{1,2}_{loc} monotonicity theorem. The proof is target independent: it uses the displayed weak gradient and the domain-variation first-variation identity, but no target-manifold structure.

The main user-facing objects are:

• LocallyMemLpTwoIn
• GradientLocallyMemLpTwoIn
• CompactlySupportedC1In
• DistributionalWeakGradientIn
• DomainVariationStationaryIn
• W12LocMapWitness
• StationaryW12LocMap
• stationaryW12LocMonotonicityFormula_euclidean
• stationaryW12LocMonotonicity_euclidean
• stationarySobolevMonotonicityFormula_euclidean
• stationarySobolevMonotonicity_euclidean

Implementation-route theorems in the radial/coarea files should normally be treated as internal scaffolding.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.stationarySobolevMonotonicityFormula_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Omega : Set (Domain n)} {a : Domain n} {R0 s r : ℝ} (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) (hOmega_meas : MeasurableSet Omega) (hclosedBall_subset : (Metric.closedBall a R0).Subset Omega) (hs_pos : 0 < s) (hsr : s < r) (hr_lt : r < R0) : weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r

Componentwise convenience wrapper for the witness-style monotonicity formula.

The preferred public API is stationaryW12LocMonotonicityFormula_euclidean, where the chosen weak gradient is bundled in a StationaryW12LocMap. This theorem keeps the old componentwise calling style by constructing that witness package first.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.stationarySobolevMonotonicity_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Omega : Set (Domain n)} {a : Domain n} {R0 s r : ℝ} (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) (hOmega_meas : MeasurableSet Omega) (hclosedBall_subset : (Metric.closedBall a R0).Subset Omega) (hs_pos : 0 < s) (hsr : s ≤ r) (hr_lt : r < R0) : weakTheta Du a s ≤ weakTheta Du a r

Componentwise convenience wrapper for the witness-style monotonicity theorem.

The preferred public API is stationaryW12LocMonotonicity_euclidean, where the chosen weak gradient is bundled in a StationaryW12LocMap. This theorem keeps the old componentwise calling style by constructing that witness package first.