Basic definitions for stationary harmonic maps

Foundational measure-theoretic lemmas and the domain Euclidean space ℝⁿ used throughout the monotonicity-formula development: the vector-measure pushforward computation behind the coarea/radial representation, together with the ambient Sobolev setup on which the later files build.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.vectorMeasure_map_withDensity_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {f : α → ℝ} {φ : α → β} {s : Set β} (hf : MeasureTheory.Integrable f μ) (hφ : Measurable φ) (hs : MeasurableSet s) : ((μ.withDensityᵥ f).map φ) s = ∫ (x : α) in φ ⁻¹' s, f x ∂μ

Applying the pushforward of the signed/vector measure μ.withDensityᵥ f to a measurable set is the same as integrating f over the preimage. This is the basic computation behind the radial signed pushforward used in the coarea step.

@[reducible, inline]

abbrev LeanStationaryHarmonicMaps.StationaryHarmonicMap.Domain (n : ℕ) : Type

The domain Euclidean space ℝⁿ.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.Domain n = EuclideanSpace ℝ (Fin n)

@[reducible, inline]

abbrev LeanStationaryHarmonicMaps.StationaryHarmonicMap.Target (m : ℕ) : Type

The target Euclidean space ℝᵐ.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.Target m = EuclideanSpace ℝ (Fin m)

@[reducible, inline]

abbrev LeanStationaryHarmonicMaps.StationaryHarmonicMap.Gradient (n m : ℕ) : Type

A pointwise gradient matrix: the i-th entry is the derivative in the i-th domain coordinate, valued in the target Euclidean space. This is the object that will later be supplied by a weak derivative.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.Gradient n m = (Fin n → LeanStationaryHarmonicMaps.StationaryHarmonicMap.Target m)

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.radialVectorMeasure_apply {n : ℕ} {f : Domain n → ℝ} {R0 : ℝ} {s : Set ℝ} (hf : MeasureTheory.IntegrableOn f (Metric.ball 0 R0) MeasureTheory.volume) (hs : MeasurableSet s) : (((MeasureTheory.volume.restrict (Metric.ball 0 R0)).withDensityᵥ f).map fun (x : Domain n) => ‖x‖) s = ∫ (x : Domain n) in {x : Domain n | ‖x‖ ∈ s}, f x ∂MeasureTheory.volume.restrict (Metric.ball 0 R0)

The radial signed pushforward of an integrable density on a ball, evaluated on a measurable radius set.