Algebra instances on EuclideanSpace

Stream: Is there code for X?

[Apurva Nakade]

Do we have the following instances in mathlib?

import Mathlib.Topology.UniformSpace.Pi
import Mathlib.Analysis.InnerProductSpace.PiL2

variable {n : Type*} [Fintype n]

instance : OrderedAddCommGroup (EuclideanSpace ℝ n) := by sorry
instance : Module ℝ (EuclideanSpace ℝ n) := by sorry
instance : OrderedSMul ℝ (EuclideanSpace ℝ n) := by sorry

More generally, how does one do linear algebra with EuclideanSpace? I cannot work with n → ℝ as I need an inner product space structure.

[Yaël Dillies]

I don't think we have them but they are easy to prove. The correct way to prove them is by adding instances of the form OrderedAddCommGroup α → OrderedAddCommGroup (WithLp α).

[Apurva Nakade]

Thanks! I'll try these out.

[Apurva Nakade]

Do I need to worry about compatibility of these structures with n → ℝ?

[Eric Wieser]

We surely have the module instance

[Eric Wieser]

It's not immediately obvious to me if inheriting the order is the right thing to do morally (though certainly it won't cause any diamonds so far)

[Eric Wieser]

@Sebastien Gouezel might have an opinion

[Sébastien Gouëzel]

It's not clear to me what you want to do with the order (or even how you would define it), mathematically. Can you explain a little bit the context?

[Yury G. Kudryashov]

Get it from the pi type?

[Eric Wieser]

Yes, I think the proposal is to keep the "box" ordering that the pi type has, which feels slightly odd given we throw out the box metric

[Yury G. Kudryashov]

Note that most (all?) other instances for EuclideanSpace are invariant under rotations.

[Apurva Nakade]

I need to use this theorem docs#ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem which is stated for inner product spaces and also need docs#ConvexCone.positive which requires an order.

[Apurva Nakade]

I could just add a version of the theorem about vectors explicitly and forget about EuclideanSpace

[Apurva Nakade]

Basically the theorems about convex cones are geometric and are basis independent. But their application to LP requires the standard basis.

[Eric Wieser]

You should take the positive cone in the pi space and push it though an isomorphism

[Yury G. Kudryashov]

Do we have a version of the hyperplane separation in terms of the dual space instead of the inner product?

[Apurva Nakade]

I don't think so. In fact, the dual cone isn't even defined in the dual space but is only defined internally: docs#Set.innerDualCone

[Apurva Nakade]

Eric Wieser said:

We surely have the module instance

Do you know where this is?

[Apurva Nakade]

Ah found it docs#WithLp.instModule

I'll try to use this instance and the positive cone idea. Hopefully this should be enough :fingers_crossed:
Thanks,

[Eric Wieser]

infer_instance should have found the instance for you

[Apurva Nakade]

Yes indeed it does! I think I failed at the others and didn't try this one at all. Thanks!