Euclidean coordinate interface

This file is the local boundary between the project and mathlib's concrete EuclideanSpace API. The project still uses Domain n = EuclideanSpace ℝ (Fin n), but downstream files should prefer the wrappers here over direct calls to EuclideanSpace.*.

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

The i-th coordinate vector in the project domain ℝⁿ.

Equations

• LeanStationaryHarmonicMaps.StationaryHarmonicMap.domainCoordUnit i = EuclideanSpace.single i 1

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.inner_domainCoordUnit_right {n : ℕ} (i : Fin n) (x : Domain n) : inner ℝ x (domainCoordUnit i) = x.ofLp i

Coordinate extraction via the Euclidean inner product.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.domain_norm_sq_eq_sum {n : ℕ} (x : Domain n) : ‖x‖ ^ 2 = ∑ i : Fin n, x.ofLp i ^ 2

Squared norm as the sum of squared coordinates.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.domain_sum_sq_eq_norm_sq {n : ℕ} (x : Domain n) : ∑ i : Fin n, x.ofLp i ^ 2 = ‖x‖ ^ 2

Sum of squared coordinates as the squared norm.

theorem LeanStationaryHarmonicMaps.StationaryHarmonicMap.domain_volume_ball_zero (n : ℕ) [NeZero n] (r : ℝ) : MeasureTheory.volume (Metric.ball 0 r) = ENNReal.ofReal r ^ Fintype.card (Fin n) * ENNReal.ofReal (√Real.pi ^ Fintype.card (Fin n) / Real.Gamma (↑(Fintype.card (Fin n)) / 2 + 1))

Euclidean volume of a ball centered at the origin, exposed through the project's Domain abbreviation.