Weak Stationarity

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

The smooth domain-variation stationarity integrand |∇u|² div X - 2 ∑ᵢⱼ <∂ᵢu, ∂ⱼu> ∂ᵢXⱼ.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.SmoothStationaryIn {n m : ℕ} (u : Domain n → Target m) (Ω : Set (Domain n)) : Prop

Smooth analogue of stationarity on an open set Ω.

This is the direct Lean translation of the weak identity in the manuscript, with fderiv standing in for the weak derivative.

Equations

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

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

Stationarity integrand written directly in terms of an arbitrary gradient field Du. This is the expression used for W^{1,2}_{loc} maps.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationarityIntegrand_eq_zero_of_notMem_tsupport {n m : ℕ} (Du : Domain n → Gradient n m) {X : Domain n → Domain n} {x : Domain n} (hx : x ∉ tsupport X) : weakStationarityIntegrand Du X x = 0

The stationarity integrand vanishes outside the topological support of the test vector field. Outside tsupport X, both X and its derivative are locally zero.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakStationaryIn {n m : ℕ} (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

Weak stationarity in the domain-variation sense, stated in terms of the weak gradient field Du.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationaryIn_of_subset {n m : ℕ} {Du : Domain n → Gradient n m} {Ω Ω' : Set (Domain n)} (hstationary : WeakStationaryIn Du Ω) (hΩ_meas : MeasurableSet Ω) (hΩ'_subset : Ω' ⊆ Ω) : WeakStationaryIn Du Ω'

Weak stationarity localizes to smaller domains. The only measure-theoretic input needed here is measurability of the larger integration domain.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.LocallyIntegrableScalarIn {n : ℕ} (f : Domain n → ℝ) (Ω : Set (Domain n)) : Prop

Local integrability of a scalar function on compact subsets of Ω.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.MapLocallyL2In {n m : ℕ} (u : Domain n → Target m) (Ω : Set (Domain n)) : Prop

The L²_loc requirement for the map itself, stated as local integrability of |u|².

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.GradientLocallyL2In {n m : ℕ} (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

The L²_loc requirement for a gradient field, stated as local integrability of its Hilbert-Schmidt energy.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.GradientAEStronglyMeasurableIn {n m : ℕ} (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

The chosen weak gradient is a.e. strongly measurable on the domain. This is kept separate from local L² control: integrability of the scalar energy density alone does not imply measurability of the full gradient field.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.GradientAEStronglyMeasurableIn Du Ω = MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict Ω)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientLocallyL2In_integrableOn_compact {n m : ℕ} {Du : Domain n → Gradient n m} {Ω K : Set (Domain n)} (hgrad : GradientLocallyL2In Du Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω) : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) K MeasureTheory.volume

Local L² control of the weak gradient gives integrability of the energy on any compact subset of the domain.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientLocallyL2In_integrableOn_closedBall {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {r : ℝ} (hgrad : GradientLocallyL2In Du Ω) (hclosedBall_subset : Metric.closedBall a r ⊆ Ω) : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) (Metric.closedBall a r) MeasureTheory.volume

Local L² control of the weak gradient gives integrability of the energy on closed balls contained in the domain.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.gradientLocallyL2In_integrableOn_ball {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {r : ℝ} (hgrad : GradientLocallyL2In Du Ω) (hclosedBall_subset : Metric.closedBall a r ⊆ Ω) : MeasureTheory.IntegrableOn (fun (x : Domain n) => weakEnergyDensity Du x) (Metric.ball a r) MeasureTheory.volume

Local L² control of the weak gradient gives integrability of the energy on open balls whose closed ball is contained in the domain.

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.HasWeakGradientIn {n m : ℕ} (u : Domain n → Target m) (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

Weak coordinate-gradient relation, using compactly supported C¹ test maps.

For each coordinate direction i, the i-th component of Du is the weak derivative of u if integration by parts holds against every compactly supported target-valued test map.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocIn {n m : ℕ} (u : Domain n → Target m) (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

A concrete W^{1,2}_{loc} interface for maps with a chosen weak gradient.

Equations

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

def LeanStationaryHarmonicMaps.StationaryHarmonicMap.WeakStationaryMapIn {n m : ℕ} (u : Domain n → Target m) (Du : Domain n → Gradient n m) (Ω : Set (Domain n)) : Prop

A weak stationary map: u ∈ W^{1,2}_{loc} with weak gradient Du, and the domain-variation stationarity identity holds in terms of Du.

Equations

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

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocIn.map_locallyL2 {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : W12LocIn u Du Ω) : MapLocallyL2In u Ω

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocIn.gradient_aestronglyMeasurable {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : W12LocIn u Du Ω) : GradientAEStronglyMeasurableIn Du Ω

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocIn.gradient_locallyL2 {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : W12LocIn u Du Ω) : GradientLocallyL2In Du Ω

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.W12LocIn.hasWeakGradient {n m : ℕ} {u : Domain n → Target m} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (h : W12LocIn u Du Ω) : HasWeakGradientIn u Du Ω

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialDerivative_aestronglyMeasurable {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (a : Domain n) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict Ω)) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialDerivative Du a x) (MeasureTheory.volume.restrict Ω)

A measurable weak gradient gives a measurable radial derivative. The proof uses only measurable algebra, since the factor |x-a|⁻¹ is not continuous at a.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity_aestronglyMeasurable {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} (a : Domain n) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict Ω)) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du a x) (MeasureTheory.volume.restrict Ω)

A measurable weak gradient gives a measurable radial-energy density.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakRadialEnergyDensity_aestronglyMeasurable_on_ball_of_gradient {n m : ℕ} {Du : Domain n → Gradient n m} {Ω : Set (Domain n)} {a : Domain n} {r : ℝ} (hDu : GradientAEStronglyMeasurableIn Du Ω) (hclosedBall_subset : Metric.closedBall a r ⊆ Ω) : MeasureTheory.AEStronglyMeasurable (fun (x : Domain n) => weakRadialEnergyDensity Du a x) (MeasureTheory.volume.restrict (Metric.ball a r))

On a ball, radial-energy measurability follows from gradient measurability on any containing closed ball/domain.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.weakStationarityIntegrand_radialVectorField {n m : ℕ} (Du : Domain n → Gradient n m) {phi : ℝ → ℝ} (hphi : Differentiable ℝ phi) (x : Domain n) : x ≠ 0 → weakStationarityIntegrand Du (radialVectorField phi) x = ((↑n - 2) * phi ‖x‖ + ‖x‖ * deriv phi ‖x‖) * weakEnergyDensity Du x - 2 * (‖x‖ * deriv phi ‖x‖ * weakRadialEnergyDensity Du 0 x)

Pointwise simplification of the weak stationarity integrand for the radial test field X(x)=φ(|x|)x, away from the origin.