Banach-Mazur Rotation Problem #
References:
- arxiv/math.0110202 A note on Banach--Mazur problem by Beata Randrianantoanina
- mathoverflow/41211 Easy proof of the fact that isotropic spaces are Euclidean
instance
Arxiv.«math.0110202».instMulActionLinearIsometryEquivRealIdElemSphereOfNat_formalConjectures
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
:
MulAction (E ≃ₗᵢ[ℝ] E) ↑(Metric.sphere 0 1)
The group of linear isometric equivalences acts on the unit sphere by evaluation.
Equations
- Arxiv.«math.0110202».instMulActionLinearIsometryEquivRealIdElemSphereOfNat_formalConjectures = { smul := fun (T : E ≃ₗᵢ[ℝ] E) (x : ↑(Metric.sphere 0 1)) => ⟨T ↑x, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }
theorem
Arxiv.«math.0110202».banach_mazur_rotation_problem :
True ↔ ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
[TopologicalSpace.SeparableSpace E] [MulAction.IsPretransitive (E ≃ₗᵢ[ℝ] E) ↑(Metric.sphere 0 1)],
∃ (H : Type u_2) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℝ H), Nonempty (E ≃ₗᵢ[ℝ] H)
The Banach--Mazur rotation problem asks whether every separable Banach space whose group of linear isometric equivalences acts transitively on the unit sphere is linearly isometric to a Hilbert space.
theorem
Arxiv.«math.0110202».banach_mazur_rotation_problem.finite_dimensional
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[MulAction.IsPretransitive (E ≃ₗᵢ[ℝ] E) ↑(Metric.sphere 0 1)]
:
Every finite-dimensional real normed space whose isometry group acts transitively on the unit sphere is Euclidean.