Unifying `tangent_cone_at` and `pos_tangent_cone_at`

Stream: maths

[Yury G. Kudryashov]

I'd like to prove more properties of tangent cones. With the definitions we have now, I'll have to prove every fact twice: once for tangent_cone_at, and once for pos_tangent_cone_at. I see two ways to unify these definitions:

1. Introduce (M : submonoid 𝕜) in the definition, and require c n ∈ M. This requires coercions here and there.
2. Define semifields and normed semifields, then pos_tangent_cone_at becomes tangent_cone_at nnreal.

The second approach looks like the right way to do it but it requires a lot of refactoring. What do you think?

BTW, is there any technical reason to have module and vector_space instead of always dealing with a semimodule?

[Johan Commelin]

Re semimodule: No, I don't think so. It's just to create a (useful, I think?) air of familiarity for mathematicians

[Sebastien Gouezel]

I'd like to prove more properties of tangent cones. With the definitions we have now, I'll have to prove every fact twice: once for tangent_cone_at, and once for pos_tangent_cone_at. I see two ways to unify these definitions:

1. Introduce (M : submonoid 𝕜) in the definition, and require c n ∈ M. This requires coercions here and there.
2. Define semifields and normed semifields, then pos_tangent_cone_at becomes tangent_cone_at nnreal.

The second approach looks like the right way to do it but it requires a lot of refactoring. What do you think?

I would go for the first way: in any case, there will be coercions involved (in the second approach, you would need to see a real module as an nnreal semimodule), so let's keep it as simple as it can be.

[Sebastien Gouezel]

BTW, is there any technical reason to have module and vector_space instead of always dealing with a semimodule?

I have tried to make module and vector_space all abbreviations for semimodule, but some things became too slow. I still think this is a good move, but it will probably have to wait for Lean 4. Link to the conversation: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear.20maps.20over.20semimodule/near/185824677