Stationary Sobolev map monotonicity

This file records the original weak-map monotonicity endpoint used by the newer public witness API. The proof is split across smaller modules below this import.

The current proved endpoint is weakTheta_le_of_arbitrary_center_W12Loc_euclidean. Future Sobolev bridge modules should discharge its WeakStationaryMapIn hypothesis and then call this theorem, rather than reopening the radial monotonicity proof chain.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_le_of_W12Loc_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 s r : ℝ} (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hs_pos : 0 < s) (hsr : s ≤ r) (hr_lt : r < R0) : weakTheta Du 0 s ≤ weakTheta Du 0 r

Euclidean-target weak monotonicity in interval form for domain-variation stationary Sobolev maps.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_le_of_centered_W12Loc_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {R0 s r : ℝ} (hmap_centered : WeakStationaryMapIn (fun (x : Domain n) => u (a + x)) (translateGradient a Du) (centeredDomain a Ω)) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall a R0 ⊆ Ω) (hs_pos : 0 < s) (hsr : s ≤ r) (hr_lt : r < R0) : weakTheta Du a s ≤ weakTheta Du a r

Auxiliary arbitrary-center Euclidean weak monotonicity in interval form for an already recentered weak stationary map package. The public theorem below automatically builds this recentered package from WeakStationaryMapIn u Du Ω.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_increment_eq_weakMonotonicityRhs_of_centered_W12Loc_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {R0 s r : ℝ} (hmap_centered : WeakStationaryMapIn (fun (x : Domain n) => u (a + x)) (translateGradient a Du) (centeredDomain a Ω)) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall a R0 ⊆ Ω) (hs_pos : 0 < s) (hsr : s < r) (hr_lt : r < R0) : weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r

Auxiliary arbitrary-center Euclidean weak increment formula for an already recentered weak stationary map package.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_le_of_arbitrary_center_W12Loc_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {R0 s r : ℝ} (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall a R0 ⊆ Ω) (hs_pos : 0 < s) (hsr : s ≤ r) (hr_lt : r < R0) : weakTheta Du a s ≤ weakTheta Du a r

Frozen public endpoint for the current custom weak interface: arbitrary- center Euclidean weak monotonicity in interval form, directly from the original-coordinate weak stationary map package.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_increment_eq_weakMonotonicityRhs_of_arbitrary_center_W12Loc_euclidean {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {R0 s r : ℝ} (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall a R0 ⊆ Ω) (hs_pos : 0 < s) (hsr : s < r) (hr_lt : r < R0) : weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r

Frozen public endpoint for the current custom weak interface: arbitrary- center Euclidean weak monotonicity formula in increment form, directly from the original-coordinate weak stationary map package.