Instances for EuclideanSpace

Stream: mathlib4

[Sebastian Kumar]

I was working with EuclideanSpace and I would like to have access to the following instances:

import Mathlib

variable {𝕜 : Type*} [RCLike 𝕜]

instance (n : ℕ) : Infinite (EuclideanSpace 𝕜 (Fin (n + 1))) :=
  PreconnectedSpace.infinite

instance (n : ℕ) : Fact (Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n) :=
  ⟨finrank_euclideanSpace_fin⟩

In particular, the second allows the use of stereographic projection in EuclideanSpace (stereographic' from Mathlib.Geometry.Manifold.Instances.Sphere). However, @Kenny Lau pointed out to me why certain theorems aren't given instances. Do the above instances have the right level of generality to be added to Mathlib? If so, where would I add them? I was thinking the second could go after the definition of finrank_euclideanSpace_fin in Mathlib.Analysis.InnerProductSpace.PiL2, but I wasn't sure about the first.

[Kenny Lau]

See the comment I left on your PR for the first one

[Kenny Lau]

I don't see the point of the second one. We shouldn't just add every Fact to Mathlib

[Sebastian Kumar]

The second one was because the definition of stereographic' needs such a Fact as an implicit argument. Is there a better way to get around this?

[Kenny Lau]

aha, in that case, yes, please PR with that justification

[Wuyang]

Sounds like the first instance needs revisiting per Kenny’s earlier comment, but the second seems justified if it enables stereographic' directly, worth a PR with that reasoning. Also, try searching related usage patterns on LeanFinder.

[Wuyang]

@leanfinder Adding Infinite and finrank Fact instances for EuclideanSpace to support stereographic projection in Lean Mathlib

[leanfinder]

Here’s what I found:

• definition stereographic' (n : ℕ) [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) : PartialHomeomorph (sphere (0 : E) 1) (EuclideanSpace ℝ (Fin n)) := stereographic (norm_eq_of_mem_sphere v) ≫ₕ (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere v)).repr.toHomeomorph.toPartialHomeomorph "Given a natural number $n$ and a real inner product space $E$ with $\text{finrank}_{\mathbb{R}} E = n + 1$, the stereographic projection stereographic' n v centered at a point $v$ on the unit sphere in $E$ is a partial homeomorphism between the sphere (excluding $v$) and the Euclidean space $\mathbb{R}^n$.

This is obtained by composing:

1. The standard stereographic projection stereographic (which maps to the orthogonal complement $(\mathbb{R}\cdot v)^\perp$)
2. A linear isometry from $(\mathbb{R}\cdot v)^\perp$ to $\mathbb{R}^n$ given by an orthonormal basis" (score: 0.767)

• theorem stereographic'_symm_apply {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) (x : EuclideanSpace ℝ (Fin n)) : ((stereographic' n v).symm x : E) = let U : (ℝ ∙ (v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere v)).repr (‖(U.symm x : E)‖ ^ 2 + 4)⁻¹ • (4 : ℝ) • (U.symm x : E) + (‖(U.symm x : E)‖ ^ 2 + 4)⁻¹ • (‖(U.symm x : E)‖ ^ 2 - 4) • v.val := by simp [real_inner_comm, stereographic, stereographic', ← Submodule.coe_norm] "Let $E$ be a finite-dimensional real inner product space with $\text{dim}_{\mathbb{R}} E = n + 1$, and let $v$ be a point on the unit sphere in $E$. For any point $x \in \mathbb{R}^n$, the inverse stereographic projection $\text{stereographic'}_v^{-1}(x)$ is given by:
  $$
  \text{stereographic'}_v^{-1}(x) = \frac{4}{\|U^{-1}x\|^2 + 4} \cdot U^{-1}x + \frac{\|U^{-1}x\|^2 - 4}{\|U^{-1}x\|^2 + 4} \cdot v
  $$
  where $U : (\mathbb{R} \cdot v)^\perp \simeq \mathbb{R}^n$ is the linear isometry defined via an orthonormal basis for the orthogonal complement of $v$." (score: 0.755)

• theorem stereographic'_target {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) : (stereographic' n v).target = Set.univ := by simp [stereographic'] "For any natural number $n$ and a real inner product space $E$ with $\text{dim}_\mathbb{R} E = n + 1$, the target of the stereographic projection stereographic' n v centered at a point $v$ on the unit sphere in $E$ is equal to the entire Euclidean space $\mathbb{R}^n$. That is, the projection maps bijectively from the sphere (minus the point $v$) onto all of $\mathbb{R}^n$." (score: 0.747)

• instance EuclideanSpace.instChartedSpaceSphere {n : ℕ} [Fact (finrank ℝ E = n + 1)] : ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : E) 1) where atlas := {f | ∃ v : sphere (0 : E) 1, f = stereographic' n v} chartAt v := stereographic' n (-v) mem_chart_source v := by simpa using ne_neg_of_mem_unit_sphere ℝ v chart_mem_atlas v := ⟨-v, rfl⟩ "For any natural number $n$ and real inner product space $E$ with $\text{finrank}_{\mathbb{R}} E = n + 1$, the unit sphere in $E$ is a charted space modeled on the Euclidean space $\mathbb{R}^n$." (score: 0.739)

• private lemma stereographic'_neg {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) : stereographic' n (-v) v = 0 := by dsimp [stereographic'] simp only [EmbeddingLike.map_eq_zero_iff] apply stereographic_neg_apply "For a vector $v$ on the unit sphere in an $(n+1)$-dimensional real inner product space $E$, the modified stereographic projection stereographic' centered at $v$ maps the antipodal point $-v$ to the origin in $\mathbb{R}^n$. This is due to the symmetry of the stereographic projection and the properties of the orthogonal complement." (score: 0.732)

• theorem stereographic'_source {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) : (stereographic' n v).source = { v }ᶜ := by simp [stereographic'] "For any natural number $n$ and a real inner product space $E$ with $\text{finrank}_{\mathbb{R}} E = n + 1$, the source of the stereographic projection $\text{stereographic'}_n v$ centered at a point $v$ on the unit sphere in $E$ is the complement of the singleton set $\{v\}$ in the sphere. That is, the projection is defined everywhere on the sphere except at the point $v$ itself." (score: 0.731)

• theorem finrank_euclideanSpace_fin {n : ℕ} : Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n := by simp "For any field $\mathbb{K}$ satisfying the RCLike condition (which includes $\mathbb{R}$ and $\mathbb{C}$) and any natural number $n$, the finite rank of the Euclidean space $\text{EuclideanSpace}(\mathbb{K}, \text{Fin }n)$ over $\mathbb{K}$ is equal to $n$, i.e.,
  $\text{finrank}_{\mathbb{K}} (\text{EuclideanSpace}(\mathbb{K}, \text{Fin }n)) = n.$" (score: 0.725)

• instance instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere (n : ℕ) : ChartedSpace (EuclideanSpace ℝ (Fin n)) (sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) := have := Fact.mk (@finrank_euclideanSpace_fin ℝ _ (n + 1)) EuclideanSpace.instChartedSpaceSphere "For any natural number $n$, the unit sphere in the Euclidean space $\mathbb{R}^{n+1}$ is a charted space modeled on $\mathbb{R}^n$." (score: 0.721)

• theorem finrank_euclideanSpace : Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι := by simp [EuclideanSpace, PiLp, WithLp] "For any field $\mathbb{K}$ satisfying the RCLike condition (which includes $\mathbb{R}$ and $\mathbb{C}$) and any finite indexing type $\iota$, the finite rank of the Euclidean space $\text{EuclideanSpace}(\mathbb{K}, \iota)$ over $\mathbb{K}$ is equal to the cardinality of $\iota$, i.e.,
  $\text{finrank}_{\mathbb{K}} (\text{EuclideanSpace}(\mathbb{K}, \iota)) = |\iota|.$" (score: 0.720)

• instance instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere (n : ℕ) : IsManifold (𝓡 n) ω (sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) := haveI := Fact.mk (@finrank_euclideanSpace_fin ℝ _ (n + 1)) EuclideanSpace.instIsManifoldSphere "For any natural number $n$, the unit sphere in the Euclidean space $\mathbb{R}^{n+1}$ is an analytic manifold modeled on $\mathbb{R}^n$ with the analytic structure given by the model with corners $\mathfrak{R}^n$." (score: 0.714)

[Sebastian Kumar]

I thought I should update that I made the PR: https://github.com/leanprover-community/mathlib4/pull/28198. However, it seems to be falling to the CI bug from #mathlib4 > Failing CI :(.

[Bryan Gin-ge Chen]

You can try merging master into your branch again; hopefully the error will go away. If not, please report it again!