Packaged monotonicity routes

This module contains the main packaged weak monotonicity routes up to the thin-shell and primitive-cutoff interfaces.

These declarations are internal scaffolding for the proof architecture. User code should normally import MainTheorem.lean or API.lean instead of relying on a particular route theorem in this file.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_radial_identity_via_radius_formulas {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hrad : WeakRadialStationarityIdentity Du R0) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hibp_formula : WeakOneDimensionalIBPFormula Du R0) (hprimitive : WeakOneDimensionalPrimitiveTestFamily Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

End-to-end weak monotonicity route from radial stationarity, after splitting the remaining analytic content into radius coarea formulas, one-dimensional integration by parts, primitive cutoffs, and the final boundary-to-radius identity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_scalar_cutoff_identity_via_radius_formulas {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hrad : WeakRadialScalarCutoffStationarityIdentity Du R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hibp_formula : WeakOneDimensionalIBPFormula Du R0) (hprimitive : WeakOneDimensionalPrimitiveTestFamily Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Weak monotonicity from the scalar-cutoff radial stationarity identity and the split analytic ingredients.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_W12_stationary_via_radius_formulas {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hstationary : WeakStationaryIn Du (Metric.ball 0 R0)) (hW : W12LocIn u Du Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hibp_formula : WeakOneDimensionalIBPFormula Du R0) (hprimitive : WeakOneDimensionalPrimitiveTestFamily Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

W^{1,2}_{loc} weak stationarity on the ball implies weak monotonicity, provided the remaining standard radius/coarea, one-dimensional cutoff, and boundary-to-radius derivative ingredients are available.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_W12_stationaryIn_via_radius_formulas {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hstationary : WeakStationaryIn Du Ω) (hΩ_meas : MeasurableSet Ω) (hW : W12LocIn u Du Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hibp_formula : WeakOneDimensionalIBPFormula Du R0) (hprimitive : WeakOneDimensionalPrimitiveTestFamily Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Domain-level W^{1,2}_{loc} weak stationarity implies weak monotonicity on balls whose closed ball is contained in the domain, modulo the remaining standard radius/coarea and one-dimensional cutoff ingredients.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_formulas {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hibp_formula : WeakOneDimensionalIBPFormula Du R0) (hprimitive : WeakOneDimensionalPrimitiveTestFamily Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final packaged weak-map interface: a WeakStationaryMapIn on a measurable domain gives weak monotonicity on any centered ball whose closed ball lies in the domain, assuming the standard radius/coarea and one-dimensional cutoff ingredients.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_realized_ingredients {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (henergy_ibp : WeakBallEnergyIntegrationByPartsFormula Du R0) (hibp_int : WeakOneDimensionalIBPIntegrability Du R0) (hprimitive_realize : WeakPrimitiveCutoffRealization R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final packaged weak-map interface with the one-dimensional IBP and primitive-cutoff steps expanded into concrete ingredients.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_energy_calculus {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) (hprimitive_realize : WeakPrimitiveCutoffRealization R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface with the one-dimensional radius calculus bundled as a single package.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_primitive_cutoffs {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) (hprimitive_realize : WeakPrimitiveCutoffRealization R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface through primitive cutoffs only. Unlike the older scalar-cutoff route, this theorem does not assume all scalar cutoffs are flat near the origin or that all radial vector fields are C¹; each one-dimensional test function is realized by a primitive cutoff that is proved flat near the origin as part of the construction.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_constructed_primitive_cutoffs {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Same primitive-cutoff route with the interval-integral/smooth-bump realization supplied by the formalized construction.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_energy_calculus_and_constructed_primitive {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hcalc : WeakBallEnergyOneDimensionalCalculus Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface where primitive cutoffs are constructed and the only remaining one-dimensional input is the bundled energy calculus package.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_ac {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface using absolute continuity of the radius energy functions as the one-dimensional calculus input. Primitive cutoffs are constructed from interval integrals and smooth bumps.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_increment {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hinc : WeakEnergyRadiusIncrementFormula Du R0) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface using the increment/FTC form of the radius energy identities.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_annulus {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (hderiv_int : WeakEnergyRadiusDerivativeIntegrability Du R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hannulus : WeakEnergyAnnulusFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface using radius integration localized to annuli to produce the radius increment/FTC identities.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_annulus_auto {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface using radius integration localized to annuli, with the annulus formula generated automatically from the W^{1,2}_{loc} hypotheses.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_annulus_ballIntegralAC {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (hball_ac : BallIntegralRadiusACOfIntegrableOnBall n) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface using the generic L¹ ball-integral AC theorem to generate radius absolute continuity from W^{1,2}_{loc} automatically.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radius_annulus_radialShellsVolume {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hflat : ScalarCutoffsConstNearOrigin R0) (hthin : RadialOpenShellsVolumeTendstoZero n) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface where radius absolute continuity is generated from the thin radial-shell volume estimate.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radialShellsVolume_vectorFieldContDiff {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hX : RadialVectorFieldContDiffForCutoffs n R0) (hthin : RadialOpenShellsVolumeTendstoZero n) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final weak-map interface where the false global flat-cutoff assumption is replaced by the exact radial-vector-field regularity input needed for stationarity tests.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_from_weakStationaryMapIn_via_radialShellsVolume_primitiveCutoffs {n m : ℕ} [NeZero n] {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {R0 : ℝ} (hR0_nonneg : 0 ≤ R0) (hmap : WeakStationaryMapIn u Du Ω) (hΩ_meas : MeasurableSet Ω) (hclosedBall_subset : Metric.closedBall 0 R0 ⊆ Ω) (hthin : RadialOpenShellsVolumeTendstoZero n) (henergy_radius : WeakEnergyRadiusIntegralFormula Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du 0 rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hderive : WeakBoundaryIdentity Du 0 R0 → ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r) : MonotoneOn (weakTheta Du 0) (Set.Ioo 0 R0)

Final packaged weak-map interface through primitive cutoffs and thin radial-shell volume control. This is the current W^{1,2}_{loc} route without the old global hflat assumption and without the replacement global hX assumption.