Boundary and radius interfaces

This module contains the boundary identities and the abstract one-dimensional radius/coarea interfaces used by the weak monotonicity proof.

These interfaces are internal scaffolding: they expose the intermediate boundary and radius statements so the proof can be checked modularly, but they are not intended as the public API of the project.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.BoundaryIdentity {n m : ℕ} (u : Domain n → Target m) (a : Domain n) (R0 : ℝ) : Prop

The a.e. boundary identity rho E'(rho) - (n-2) E(rho) = 2 rho Q'(rho).

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakBoundaryIdentity {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (R0 : ℝ) : Prop

Weak a.e. boundary identity, stated directly in terms of the weak gradient energy and weak radial energy.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakBoundaryRadiusIdentityAt {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (rho : ℝ) : Prop

The weak boundary identity at one fixed radius.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakSharpCutoffRadiusIdentityAt {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (rho : ℝ) : Prop

The signed identity at one fixed radius produced by the decreasing sharp-cutoff approximation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffDefect {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (rho : ℝ) : ℝ

The scalar defect whose vanishing is the sharp-cutoff radius identity.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffRadiusIdentityAt_iff_defect_eq_zero {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {rho : ℝ} : WeakSharpCutoffRadiusIdentityAt Du a rho ↔ weakSharpCutoffDefect Du a rho = 0

Vanishing of the defect is exactly the signed sharp-cutoff identity at one radius.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffRadiusIdentityAt_of_defect_eq_zero {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {rho : ℝ} (h : weakSharpCutoffDefect Du a rho = 0) : WeakSharpCutoffRadiusIdentityAt Du a rho

Pointwise conversion from vanishing defect to the signed sharp-cutoff radius identity.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakSharpCutoffLimitIdentity {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (R0 : ℝ) : Prop

The a.e. identity obtained from the radial stationarity identity by testing with smooth radial cutoffs approximating the sharp cutoff of B_r(a).

The sign reflects the fact that the approximating cutoffs decrease from 1 to 0, so their derivatives converge to -δ_r.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakSharpCutoffDistributionIdentity {n m : ℕ} (Du : Domain n → Gradient n m) (a : Domain n) (R0 : ℝ) : Prop

Distributional form of the sharp-cutoff limit: the sharp-cutoff defect pairs to zero against every compactly supported smooth test function in (0, R0).

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffLimitIdentity_of_distribution {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 : ℝ} (hdefect_loc : MeasureTheory.LocallyIntegrableOn (fun (rho : ℝ) => weakSharpCutoffDefect Du a rho) (Set.Ioo 0 R0) MeasureTheory.volume) (hdist : WeakSharpCutoffDistributionIdentity Du a R0) : WeakSharpCutoffLimitIdentity Du a R0

If the sharp-cutoff defect is locally integrable and vanishes as a distribution on (0, R0), then the sharp-cutoff radius identity holds a.e.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBoundaryRadiusIdentityAt_of_sharpCutoff {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {rho : ℝ} (h : WeakSharpCutoffRadiusIdentityAt Du a rho) : WeakBoundaryRadiusIdentityAt Du a rho

Pointwise algebra from the signed sharp-cutoff identity to the boundary identity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffRadiusIdentityAt_of_boundary {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {rho : ℝ} (h : WeakBoundaryRadiusIdentityAt Du a rho) : WeakSharpCutoffRadiusIdentityAt Du a rho

Pointwise algebra from the boundary identity back to the signed sharp-cutoff form.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakBoundaryIdentity_of_sharpCutoffLimit {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 : ℝ} (hlimit : WeakSharpCutoffLimitIdentity Du a R0) : WeakBoundaryIdentity Du a R0

The sharp-cutoff limit form is just the boundary identity with all terms moved across the equality.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffLimit_of_boundaryIdentity {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 : ℝ} (hboundary : WeakBoundaryIdentity Du a R0) : WeakSharpCutoffLimitIdentity Du a R0

Conversely, the boundary identity can be written in the signed sharp-cutoff-limit form used by the approximation argument.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakSharpCutoffLimitIdentity_iff_boundaryIdentity {n m : ℕ} {Du : Domain n → Gradient n m} {a : Domain n} {R0 : ℝ} : WeakSharpCutoffLimitIdentity Du a R0 ↔ WeakBoundaryIdentity Du a R0

Algebraic equivalence between the sharp-cutoff limit identity and the weak boundary identity.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialCutoffLimitStep {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The analytic cutoff-limit step still to be supplied: approximate the sharp radial cutoff in the weak radial stationarity identity and pass to a.e. radii.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialOneDimensionalMainIntegrand {n m : ℕ} (Du : Domain n → Gradient n m) (phi : ℝ → ℝ) (rho : ℝ) : ℝ

Main one-dimensional radial integrand after applying coarea.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialOneDimensionalRhsIntegrand {n m : ℕ} (Du : Domain n → Gradient n m) (phi : ℝ → ℝ) (rho : ℝ) : ℝ

Radial-energy one-dimensional integrand after applying coarea.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialOneDimensionalIdentity {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

One-dimensional radius form of the weak radial identity. This is the coarea/absolute-continuity form of WeakRadialStationarityIdentity: the ball integrals have been converted into derivatives of the ball energy functions.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialScalarCutoffStationarityIdentity {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Weak radial stationarity restricted to the scalar cutoff class used by the one-dimensional sharp-cutoff argument. This is the W^{1,2}_{loc}-friendly entry point: the vector-field regularity and integrability are discharged before this interface.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialCoareaDerivativeFormula {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The concrete coarea/radius-derivative formula needed to turn the spatial radial identity into its one-dimensional radius form. This is the place where a future polar-coordinate or coarea formalization should plug in.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialVectorFieldContDiffForCutoffs (n : ℕ) (R0 : ℝ) : Prop

Regularity of the radial vector field for the scalar cutoffs used in the one-dimensional argument. The support properties are automatic from tsupport phi ⊆ Iio R0; this predicate only records the remaining C¹ fact.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.ScalarCutoffsConstNearOrigin (R0 : ℝ) : Prop

The scalar cutoffs used for the radial vector-field tests are flat at the origin. This is the natural condition ensuring that phi(|x|) x is C¹ at x = 0.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorFieldContDiffForCutoffs_of_constNearOrigin {n : ℕ} {R0 : ℝ} (hflat : ScalarCutoffsConstNearOrigin R0) : RadialVectorFieldContDiffForCutoffs n R0

Flatness at the origin discharges the radial vector-field C¹ regularity ingredient.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_scalar_cutoff_identity_from_stationarity_of_W12Loc {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) : WeakRadialScalarCutoffStationarityIdentity Du R0

Weak W^{1,2}_{loc} stationarity gives the scalar-cutoff radial identity for every cutoff in the flat-at-origin class used by the sharp-cutoff argument.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weak_radial_scalar_cutoff_identity_from_stationarity_of_W12Loc_vectorFieldContDiff {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 ⊆ Ω) (hX : RadialVectorFieldContDiffForCutoffs n R0) : WeakRadialScalarCutoffStationarityIdentity Du R0

Weak W^{1,2}_{loc} stationarity gives the scalar-cutoff radial identity once the radial vector fields for the scalar cutoffs are known to be C¹. This avoids the false global assumption that every scalar cutoff is flat near the origin.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialCoareaIntegralFormula {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The true coarea/radius-integral content, separated from vector-field regularity and support bookkeeping.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.thetaFactor_indicator_aestronglyMeasurable {n : ℕ} {R0 s r : ℝ} (hs : 0 < s) : MeasureTheory.AEStronglyMeasurable ((Set.Ioo s r).indicator (thetaFactor n)) (radiusIntervalMeasure R0)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radiusWeightOn_indicator_thetaFactor {n : ℕ} {R0 s r : ℝ} (hs : 0 < s) : RadiusWeightOn R0 ((Set.Ioo s r).indicator (thetaFactor n))

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakEnergyRadiusIntegralFormula {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Radius-integration formula for weak energy density. This is the exact coarea/ball-derivative statement needed for the energy part.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakEnergyRadiusIntegralFormulaForWeights {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Radius-integration formula for weak energy density, restricted to measurable essentially bounded radius weights.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialEnergyRadiusIntegralFormula {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Radius-integration formula for weak radial-energy density.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialEnergyRadiusIntegralFormulaForWeights {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

Radius-integration formula for weak radial-energy density, restricted to measurable essentially bounded radius weights.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadiusIntegralFormulas {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The two radius-derivative/coarea formulas needed for the weak monotonicity argument, bundled as a single reusable analytic input.

Equations

• One or more equations did not get rendered due to their size.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadiusIntegralFormulasForWeights {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The restricted-weight version of the bundled radius formulas.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyRadiusIntegralFormulaForWeights_of_unrestricted {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (henergy : WeakEnergyRadiusIntegralFormula Du R0) : WeakEnergyRadiusIntegralFormulaForWeights Du R0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyRadiusIntegralFormulaForWeights_of_unrestricted {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hradial : WeakRadialEnergyRadiusIntegralFormula Du R0) : WeakRadialEnergyRadiusIntegralFormulaForWeights Du R0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadiusIntegralFormulasForWeights_of_unrestricted {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hradius : WeakRadiusIntegralFormulas Du R0) : WeakRadiusIntegralFormulasForWeights Du R0

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialCoareaIntegralFormula_of_radiusIntegral {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (henergy : WeakEnergyRadiusIntegralFormula Du R0) (hradial : WeakRadialEnergyRadiusIntegralFormula Du R0) : WeakRadialCoareaIntegralFormula Du R0

The two standard radius-integration formulas imply the coarea integral formula for the radial stationarity coefficients.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialCoareaIntegralFormula_of_radiusIntegralForWeights {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (henergy : WeakEnergyRadiusIntegralFormulaForWeights Du R0) (hradial : WeakRadialEnergyRadiusIntegralFormulaForWeights Du R0) : WeakRadialCoareaIntegralFormula Du R0

The restricted radius-integration formulas are enough for the scalar-cutoff coarea step, because the two cutoff coefficients are measurable essentially bounded radius weights.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialCoareaIntegralFormula_of_radiusIntegralFormulas {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hradius : WeakRadiusIntegralFormulas Du R0) : WeakRadialCoareaIntegralFormula Du R0

Bundled radius-integration formulas imply the coarea integral formula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialCoareaIntegralFormula_of_radiusIntegralFormulasForWeights {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hradius : WeakRadiusIntegralFormulasForWeights Du R0) : WeakRadialCoareaIntegralFormula Du R0

Bundled restricted radius-integration formulas imply the scalar-cutoff coarea integral formula.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialOneDimensionalIdentity_of_scalar_cutoff_and_coarea {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hrad : WeakRadialScalarCutoffStationarityIdentity Du R0) (hcoarea : WeakRadialCoareaIntegralFormula Du R0) : WeakRadialOneDimensionalIdentity Du R0

The scalar-cutoff radial stationarity identity plus the coarea/radius integral formula gives the one-dimensional radius identity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialOneDimensionalIdentity_of_scalar_cutoff_and_radiusIntegralForWeights {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hrad : WeakRadialScalarCutoffStationarityIdentity Du R0) (henergy : WeakEnergyRadiusIntegralFormulaForWeights Du R0) (hradial : WeakRadialEnergyRadiusIntegralFormulaForWeights Du R0) : WeakRadialOneDimensionalIdentity Du R0

Restricted radius-integration formulas plus the scalar-cutoff radial stationarity identity give the one-dimensional radius identity.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialCoareaDerivativeFormula_of_contDiff_and_integral {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hX : RadialVectorFieldContDiffForCutoffs n R0) (hcoarea : WeakRadialCoareaIntegralFormula Du R0) : WeakRadialCoareaDerivativeFormula Du R0

Vector-field regularity plus the coarea/radius-integral formula gives the combined coarea derivative formula used by the radial-to-boundary route.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakRadialCoareaDerivativeStep {n m : ℕ} (Du : Domain n → Gradient n m) (R0 : ℝ) : Prop

The coarea and radius-derivative step translating the spatial radial identity into its one-dimensional radius form.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialCoareaDerivativeStep_of_formula {n m : ℕ} {Du : Domain n → Gradient n m} {R0 : ℝ} (hformula : WeakRadialCoareaDerivativeFormula Du R0) : WeakRadialCoareaDerivativeStep Du R0

A concrete radial coarea/radius-derivative formula discharges the abstract coarea step.