Final monotonicity increment

This module contains the final radius integration step and converts the boundary identity into monotonicity of the weak theta quantity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.interior_monotonicity_formula_smooth {n m : ℕ} {u : Domain n → Target m} {a : Domain n} {R0 s r : ℝ} (hu : ContDiff ℝ 1 u) (hboundary : BoundaryIdentity u a R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) (hderive : ContDiff ℝ 1 u → BoundaryIdentity u a R0 → 0 < s → s < r → r < R0 → theta u a r - theta u a s = monotonicityRhs u a s r) : theta u a r - theta u a s = monotonicityRhs u a s r

Step 4: integrate the a.e. derivative formula for theta.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.interior_monotonicity_formula_weak {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 s r : ℝ} (hboundary : WeakBoundaryIdentity Du a R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) (hderive : WeakBoundaryIdentity Du a R0 → 0 < s → s < r → r < R0 → weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r) : weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r

Weak version of the final integration step, using weakTheta and the weak annular radial-energy term.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_increment_eq_radius_integral_of_boundary {n m : ℕ} {Du : Domain n → Gradient n m} {R0 s r : ℝ} (hboundary : WeakBoundaryIdentity Du 0 R0) (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) : weakTheta Du 0 r - weakTheta Du 0 s = ∫ (rho : ℝ) in s..r, 2 * thetaFactor n rho * deriv (weakBallRadialEnergy Du 0) rho

Radius-variable form of the final monotonicity increment. This integrates the a.e. boundary identity against the derivative of the monotonicity weight; the remaining step is to convert the right-hand side to the annular spatial integral.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radial_weighted_annulus_integral_eq_indicator_integral {n : ℕ} [NeZero n] {F : Domain n → ℝ} {s r R0 : ℝ} (hrR0 : r ≤ R0) : ∫ (x : Domain n) in Metric.ball 0 R0, (Set.Ioo s r).indicator (fun (rho : ℝ) => thetaFactor n rho) ‖x‖ * F x = ∫ (x : Domain n) in Metric.ball 0 r \ Metric.ball 0 s, thetaFactor n ‖x‖ * F x

A radial indicator on the containing ball is the same as integrating over the annulus. The inner boundary sphere is null in positive dimension.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakMonotonicityRhs_eq_radius_integral {n m : ℕ} [NeZero n] {Du : Domain n → Gradient n m} {R0 s r : ℝ} (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) : weakMonotonicityRhs Du 0 s r = 2 * ∫ (rho : ℝ) in s..r, thetaFactor n rho * deriv (weakBallRadialEnergy Du 0) rho

The annular term in the monotonicity formula is exactly the corresponding radius integral of the radial-energy derivative.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakMonotonicityRhs_eq_radius_integral_forWeights {n m : ℕ} [NeZero n] {Du : Domain n → Gradient n m} {R0 s r : ℝ} (hradial_radius : WeakRadialEnergyRadiusIntegralFormulaForWeights Du R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) : weakMonotonicityRhs Du 0 s r = 2 * ∫ (rho : ℝ) in s..r, thetaFactor n rho * deriv (weakBallRadialEnergy Du 0) rho

Restricted-weight version of the conversion from the annular spatial term to the radius integral of the radial-energy derivative.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_increment_eq_weakMonotonicityRhs_of_boundary {n m : ℕ} [NeZero n] {Du : Domain n → Gradient n m} {R0 s r : ℝ} (hboundary : WeakBoundaryIdentity Du 0 R0) (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormula Du R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) : weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r

The final increment formula derived from the weak boundary identity, radius absolute continuity, and the radial-energy radius formula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_increment_eq_weakMonotonicityRhs_of_boundary_forWeights {n m : ℕ} [NeZero n] {Du : Domain n → Gradient n m} {R0 s r : ℝ} (hboundary : WeakBoundaryIdentity Du 0 R0) (hac : WeakEnergyAbsolutelyContinuousOnRadii Du R0) (hradial_radius : WeakRadialEnergyRadiusIntegralFormulaForWeights Du R0) (hs : 0 < s) (hsr : s < r) (hr : r < R0) : weakTheta Du 0 r - weakTheta Du 0 s = weakMonotonicityRhs Du 0 s r

Restricted-weight version of the final increment formula derived from the weak boundary identity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.theta_monotone_on_of_formula {n m : ℕ} {u : Domain n → Target m} {a : Domain n} {R0 : ℝ} (hformula : ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → theta u a r - theta u a s = monotonicityRhs u a s r) (hrhs_nonneg : ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → 0 ≤ monotonicityRhs u a s r) : MonotoneOn (theta u a) (Set.Ioo 0 R0)

The equality formula immediately gives monotonicity, because the annular integral is nonnegative.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_on_of_formula {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 : ℝ} (hformula : ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r) (hrhs_nonneg : ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → 0 ≤ weakMonotonicityRhs Du a s r) : MonotoneOn (weakTheta Du a) (Set.Ioo 0 R0)

Weak monotonicity follows from the weak equality formula and nonnegativity of the weak annular radial-energy term.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakTheta_monotone_on_of_formula' {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 : ℝ} (hformula : ∀ ⦃s r : ℝ⦄, 0 < s → s < r → r < R0 → weakTheta Du a r - weakTheta Du a s = weakMonotonicityRhs Du a s r) : MonotoneOn (weakTheta Du a) (Set.Ioo 0 R0)

Clean weak monotonicity interface: once the weak equality formula is known, monotonicity follows from the built-in nonnegativity of the radial-energy RHS.