Dimensions of Euclidean spaces

The first lemma derives positive ambient dimension from a nonzero vector. In particular, a nonzero displacement supplies the dimension hypothesis needed for Newtonian-kernel monotonicity and Poisson-kernel positivity.

The instance TauCeti.factFinrankEuclideanSpaceComplex records the real dimension of ℂᵏ⁺¹ as (2k + 1) + 1. This is the form of the hypothesis Fact (finrank ℝ E = n + 1) under which Mathlib puts a manifold structure on the unit sphere of E (EuclideanSpace.instChartedSpaceSphere), so instance search finds the sphere of ℂᵏ⁺¹, and its quotients, to be manifolds of dimension 2k + 1.

theorem TauCeti.pos_of_ne_zero_euclideanSpace {n : ℕ} {x : EuclideanSpace ℝ (Fin n)} (hx : x ≠ 0) : 0 < n

A nonzero vector in EuclideanSpace ℝ (Fin n) forces the dimension to be positive.

instance TauCeti.factFinrankEuclideanSpaceComplex (k : ℕ) : Fact (Module.finrank ℝ (EuclideanSpace ℂ (Fin (k + 1))) = 2 * k + 1 + 1)

The real dimension of ℂᵏ⁺¹ is 2k + 2, written as (2k + 1) + 1 so that its unit sphere, and quotients of the sphere, are found to be manifolds of dimension 2k + 1.