Radial Geometry

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.coordUnit {n : ℕ} (i : Fin n) : Domain n

The i-th coordinate vector in ℝⁿ.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.coordUnit i = LeanStationaryHarmonicMaps.StationaryHarmonicMap.domainCoordUnit i

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative {n m : ℕ} (u : Domain n → Target m) (i : Fin n) (x : Domain n) : Target m

The classical coordinate derivative ∂ᵢ u, in the smooth model.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative u i x = (fderiv ℝ u x) (LeanStationaryHarmonicMaps.StationaryHarmonicMap.coordUnit i)

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.vectorFieldPartial {n : ℕ} (X : Domain n → Domain n) (i j : Fin n) (x : Domain n) : ℝ

Coordinate derivative of a vector field component: ∂ᵢ Xⱼ.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.vectorFieldPartial X i j x = (LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative X i x).ofLp j

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.divergence {n : ℕ} (X : Domain n → Domain n) (x : Domain n) : ℝ

Divergence of a smooth vector field in coordinates: div X = ∑ᵢ ∂ᵢ Xᵢ.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.divergence X x = ∑ i : Fin n, LeanStationaryHarmonicMaps.StationaryHarmonicMap.vectorFieldPartial X i i x

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialUnit {n : ℕ} (a x : Domain n) : Domain n

The radial unit vector based at a. At x = a this definition gives 0, which is harmless for integral identities.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialUnit a x = ‖x - a‖⁻¹ • (x - a)

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientEnergy {n m : ℕ} (A : Gradient n m) : ℝ

Pointwise Hilbert-Schmidt energy of a gradient matrix.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientEnergy A = ∑ i : Fin n, ‖A i‖ ^ 2

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialDerivative {n m : ℕ} (A : Gradient n m) (x : Domain n) : Target m

Radial derivative associated to a pointwise gradient matrix, evaluated in the radial direction from the origin to x.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialDerivative A x = SMul.smul ‖x‖⁻¹ (∑ i : Fin n, SMul.smul (x.ofLp i) (A i))

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialEnergy {n m : ℕ} (A : Gradient n m) (x : Domain n) : ℝ

Radial energy associated to a pointwise gradient matrix.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialEnergy A x = ‖LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialDerivative A x‖ ^ 2

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.smoothGradient {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : Gradient n m

A smooth map gives a pointwise gradient matrix by classical coordinate derivatives.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.smoothGradient u x i = LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative u i x

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyDensity {n m : ℕ} (Du : Domain n → Gradient n m) (x : Domain n) : ℝ

Energy density built from an arbitrary gradient field.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakEnergyDensity Du x = LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientEnergy (Du x)

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialDerivative {n m : ℕ} (Du : Domain n → Gradient n m) (a x : Domain n) : Target m

Radial derivative built from an arbitrary gradient field.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialDerivative Du a x = LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialDerivative (Du x) (x - a)

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

Radial energy density built from an arbitrary gradient field.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity Du a x = ‖LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialDerivative Du a x‖ ^ 2

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialDerivative {n m : ℕ} (u : Domain n → Target m) (a x : Domain n) : Target m

Smooth-model radial derivative of u based at a.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialDerivative u a x = (fderiv ℝ u x) (LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialUnit a x)

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.energyDensity {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : ℝ

Smooth-model Dirichlet energy density: |∇u|² = ∑ᵢ |∂ᵢ u|².

Do not replace this by the operator norm squared of fderiv; the Dirichlet energy density uses the Hilbert-Schmidt/Frobenius norm of the derivative.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.energyDensity u x = ∑ i : Fin n, ‖LeanStationaryHarmonicMaps.StationaryHarmonicMap.partialDerivative u i x‖ ^ 2

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialEnergyDensity {n m : ℕ} (u : Domain n → Target m) (a x : Domain n) : ℝ

Radial energy density of a smooth map: the squared norm of its radial derivative.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialEnergyDensity u a x = ‖LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialDerivative u a x‖ ^ 2

noncomputable def LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField {n : ℕ} (phi : ℝ → ℝ) (x : Domain n) : Domain n

The radial test vector field X(x) = φ(|x|) x, centered at the origin.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorField phi x = phi ‖x‖ • x

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.fderiv_norm_apply {n : ℕ} {x v : Domain n} (hx : x ≠ 0) : (fderiv ℝ (fun (y : Domain n) => ‖y‖) x) v = inner ℝ x v / ‖x‖

The differential of the Euclidean norm away from the origin: d|x|(v) = <x,v>/|x|.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.fderiv_phi_norm_apply {n : ℕ} {phi : ℝ → ℝ} {x v : Domain n} (hphi : DifferentiableAt ℝ phi ‖x‖) (hx : x ≠ 0) : (fderiv ℝ (fun (y : Domain n) => phi ‖y‖) x) v = deriv phi ‖x‖ * (inner ℝ x v / ‖x‖)

The differential of phi |x| away from the origin.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialVectorFieldDerivativeFormula {n : ℕ} (phi : ℝ → ℝ) : Prop

Component-wise derivative formula for X(x) = φ(|x|) x.

This is the formal version of ∂ᵢ Xⱼ = φ(r) δᵢⱼ + φ'(r) xᵢ xⱼ / r.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorFieldDerivativeFormula {n : ℕ} {phi : ℝ → ℝ} (hphi : Differentiable ℝ phi) : RadialVectorFieldDerivativeFormula phi

Proof of ∂ᵢ(φ(|x|) xⱼ) = φ(|x|) δᵢⱼ + φ'(|x|) xᵢxⱼ/|x|.

This is exactly the coordinate computation in the manuscript: differentiate the product φ(r) xⱼ, use ∂ᵢ r = xᵢ/r, and then rewrite δᵢⱼ as the j-th component of eᵢ.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialVectorFieldDivergenceFormula {n : ℕ} (phi : ℝ → ℝ) : Prop

Divergence formula for the radial vector field: div X = n φ(r) + r φ'(r).

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorFieldDivergenceFormula {n : ℕ} {phi : ℝ → ℝ} (hphi : Differentiable ℝ phi) : RadialVectorFieldDivergenceFormula phi

Proof of div (φ(|x|)x) = n φ(|x|) + |x| φ'(|x|).

This is obtained by taking j = i in RadialVectorFieldDerivativeFormula and summing over i.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.euclideanSpace_sum_coordUnit {n : ℕ} (x : Domain n) : ∑ i : Fin n, SMul.smul (x.ofLp i) (coordUnit i) = x

Coordinate expansion in the standard basis of EuclideanSpace.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.fderiv_apply_eq_sum_partial {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : (fderiv ℝ u x) x = ∑ i : Fin n, SMul.smul (x.ofLp i) (partialDerivative u i x)

Apply the linear map fderiv u x to the coordinate expansion of x.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.inner_smul_smul_real {m : ℕ} (a b : ℝ) (v w : Target m) : inner ℝ (SMul.smul a v) (SMul.smul b w) = a * b * inner ℝ v w

Real scalar factors pull out of both entries of the inner product.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.norm_sq_sum_smul {n m : ℕ} (a : Fin n → ℝ) (v : Fin n → Target m) : ‖∑ i : Fin n, SMul.smul (a i) (v i)‖ ^ 2 = ∑ i : Fin n, ∑ j : Fin n, a i * a j * inner ℝ (v i) (v j)

The square norm of a finite real linear combination, expanded as a double sum.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.norm_sum_smul_le_sqrt_mul_sqrt {n m : ℕ} (a : Fin n → ℝ) (v : Fin n → Target m) : ‖∑ i : Fin n, SMul.smul (a i) (v i)‖ ≤ √(∑ i : Fin n, a i ^ 2) * √(∑ i : Fin n, ‖v i‖ ^ 2)

Cauchy-Schwarz for a finite real linear combination of target vectors.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialCoeff_sq_sum_le_one {n : ℕ} (x : Domain n) : ∑ i : Fin n, (‖x‖⁻¹ * x.ofLp i) ^ 2 ≤ 1

The squared coefficients of the radial unit direction have sum at most 1.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialEnergy_eq_sum {n m : ℕ} (A : Gradient n m) (x : Domain n) : gradientRadialEnergy A x = ‖x‖⁻¹ ^ 2 * ∑ i : Fin n, ∑ j : Fin n, x.ofLp i * x.ofLp j * inner ℝ (A i) (A j)

The radial energy of an arbitrary gradient matrix as a double contraction.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialEnergy_le_gradientEnergy {n m : ℕ} (A : Gradient n m) (x : Domain n) : gradientRadialEnergy A x ≤ gradientEnergy A

The radial part of a pointwise gradient matrix is bounded by its full Hilbert-Schmidt energy.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity_le_weakEnergyDensity {n m : ℕ} (Du : Domain n → Gradient n m) (a x : Domain n) : weakRadialEnergyDensity Du a x ≤ weakEnergyDensity Du x

The weak radial energy density is pointwise bounded by the full weak energy density.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.norm_weakRadialEnergyDensity_le_weakEnergyDensity {n m : ℕ} (Du : Domain n → Gradient n m) (a x : Domain n) : ‖weakRadialEnergyDensity Du a x‖ ≤ weakEnergyDensity Du x

Norm form of weakRadialEnergyDensity_le_weakEnergyDensity, convenient for Integrable.mono'.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialStressContractionFormula {n m : ℕ} (A : Gradient n m) (phi : ℝ → ℝ) {x : Domain n} (hx : x ≠ 0) : ∑ i : Fin n, ∑ j : Fin n, inner ℝ (A i) (A j) * (phi ‖x‖ * (coordUnit i).ofLp j + deriv phi ‖x‖ * (x.ofLp i * x.ofLp j / ‖x‖)) = phi ‖x‖ * gradientEnergy A + ‖x‖ * deriv phi ‖x‖ * gradientRadialEnergy A x

Pure pointwise algebraic contraction for a radial vector-field derivative, with an arbitrary gradient matrix A. This is the version that will survive unchanged in the W^{1,2}_{loc} proof.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialDerivative_zero_eq_sum {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : radialDerivative u 0 x = SMul.smul ‖x‖⁻¹ (∑ i : Fin n, SMul.smul (x.ofLp i) (partialDerivative u i x))

At the origin, the radial derivative is |x|⁻¹ ∑ᵢ xᵢ ∂ᵢu.

@[simp]

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientEnergy_smoothGradient {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : gradientEnergy (smoothGradient u x) = energyDensity u x

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialDerivative_smoothGradient_zero {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : gradientRadialDerivative (smoothGradient u x) x = radialDerivative u 0 x

@[simp]

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientRadialEnergy_smoothGradient_zero {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : gradientRadialEnergy (smoothGradient u x) x = radialEnergyDensity u 0 x

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialEnergyDensity_zero_eq_sum {n m : ℕ} (u : Domain n → Target m) (x : Domain n) : radialEnergyDensity u 0 x = ‖x‖⁻¹ ^ 2 * ∑ i : Fin n, ∑ j : Fin n, x.ofLp i * x.ofLp j * inner ℝ (partialDerivative u i x) (partialDerivative u j x)

The radial energy density at the origin as the double contraction |x|⁻² ∑ᵢⱼ xᵢxⱼ <∂ᵢu,∂ⱼu>.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.RadialStressContractionFormula {n m : ℕ} (u : Domain n → Target m) (phi : ℝ → ℝ) : Prop

The algebraic stress-energy contraction for the radial vector field.

This is the formal target corresponding to ∑ᵢⱼ <∂ᵢu,∂ⱼu> ∂ᵢXⱼ = φ(r)|∇u|² + rφ'(r)|∂ᵣu|².

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialStressContractionFormula {n m : ℕ} (u : Domain n → Target m) {phi : ℝ → ℝ} (hphi : Differentiable ℝ phi) : RadialStressContractionFormula u phi

Proof of the stress-energy contraction identity for X(x) = φ(|x|)x.

This is the formal version of substituting ∂ᵢXⱼ = φ(r)δᵢⱼ + φ'(r)xᵢxⱼ/r into the double contraction.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialStressContractionFormula {n m : ℕ} (Du : Domain n → Gradient n m) {phi : ℝ → ℝ} (hphi : Differentiable ℝ phi) (x : Domain n) : x ≠ 0 → ∑ i : Fin n, ∑ j : Fin n, inner ℝ (Du x i) (Du x j) * vectorFieldPartial (radialVectorField phi) i j x = phi ‖x‖ * weakEnergyDensity Du x + ‖x‖ * deriv phi ‖x‖ * weakRadialEnergyDensity Du 0 x

The stress contraction formula for an arbitrary gradient field.