Commit 2026-01-25 09:47 d8a87eeb
View on Github →refactor(TangentCone): redefine for TVS (#34127)
While the former definition of tangentConeAt was good enough for normed spaces,
it behaved well only if the space has first countable topology.
Also, we had to use two different definitions for tangentConeAt and for posTangentConeAt.
After this PR, we request that d n → 0 in the definition
instead of assuming that the norm of c n tends to infinity.
Also, we allow approximation along any filter,
not only Filter.atTop on natural numbers.
As a result, the new definition works well for topological vector spaces,
and posTangentConeAt is just the usual tangent cone
with NNReal as the coefficients semiring.
This PR is a part of a larger effort aimed to generalize large parts of our calculus library
to topological vector spaces, see https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/generalizing.20deriv.20to.20TVS/with/569179043