Main monotonicity theorem #
This file exports the witness-style public theorem. All radial, coarea, cutoff, and boundary routes are internal scaffolding hidden behind the stationary Sobolev map package.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.stationaryW12LocMonotonicityFormula_euclidean
{n m : ℕ}
[NeZero n]
{u : Domain n → Target m}
{Omega : Set (Domain n)}
(hmap : StationaryW12LocMap u Omega)
{a : Domain n}
{R0 s r : ℝ}
(hOmega_meas : MeasurableSet Omega)
(hclosedBall_subset : (Metric.closedBall a R0).Subset Omega)
(hs_pos : 0 < s)
(hsr : s < r)
(hr_lt : r < R0)
:
Main witness-style public monotonicity formula.
This is the equality form of the monotonicity theorem: the increment of
weakTheta is the nonnegative annular radial-energy term
weakMonotonicityRhs.
theorem
LeanStationaryHarmonicMaps.StationaryHarmonicMap.stationaryW12LocMonotonicity_euclidean
{n m : ℕ}
[NeZero n]
{u : Domain n → Target m}
{Omega : Set (Domain n)}
(hmap : StationaryW12LocMap u Omega)
{a : Domain n}
{R0 s r : ℝ}
(hOmega_meas : MeasurableSet Omega)
(hclosedBall_subset : (Metric.closedBall a R0).Subset Omega)
(hs_pos : 0 < s)
(hsr : s ≤ r)
(hr_lt : r < R0)
:
Main witness-style public monotonicity theorem.
The chosen weak gradient is part of the stationary Sobolev witness, and the
conclusion uses that same gradient in weakTheta.