Tangent spaces of invariant sets along a flow

Let ϕ be a flow on a real normed space whose time maps are differentiable. A flow-invariant set S, such as the stable or unstable set of a rest point, is carried onto itself by each time map ϕ t, a homeomorphism with invertible derivative Dϕ_t(x) (Flow.isInvertible_fderiv). So Dϕ_t(x) carries the tangent space of S at x, the span of its tangent cone, onto its tangent space at ϕ t x. In particular, the transversality of two invariant sets, the condition that their tangent spaces together span the whole space, holds at one point of an orbit if and only if it holds at every point of that orbit.

Main results

• Flow.span_tangentConeAt_apply: Dϕ_t(x) carries the tangent space of a flow-invariant set at x onto its tangent space at ϕ t x.
• Flow.span_tangentConeAt_sup_span_tangentConeAt_apply_eq_top_iff: two invariant sets are transverse at ϕ t x if and only if they are transverse at x.

theorem Flow.span_tangentConeAt_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} {S : Set E} (hS : IsInvariant ϕ.toFun S) (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : Submodule.span ℝ (tangentConeAt ℝ S (ϕ.toFun t x)) = Submodule.map (↑(fderiv ℝ (ϕ.toFun t) x)) (Submodule.span ℝ (tangentConeAt ℝ S x))

Tangent spaces of invariant sets along a flow. When the time-t map is differentiable at x and the time-(-t) map at ϕ t x, the derivative Dϕ_t(x) carries the tangent space at x of a flow-invariant set onto its tangent space at ϕ t x.

theorem Flow.span_tangentConeAt_sup_span_tangentConeAt_apply_eq_top_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ϕ : Flow ℝ E} {t : ℝ} {x : E} {S T : Set E} (hS : IsInvariant ϕ.toFun S) (hT : IsInvariant ϕ.toFun T) (hs : DifferentiableAt ℝ (ϕ.toFun (-t)) (ϕ.toFun t x)) (ht : DifferentiableAt ℝ (ϕ.toFun t) x) : Submodule.span ℝ (tangentConeAt ℝ S (ϕ.toFun t x)) ⊔ Submodule.span ℝ (tangentConeAt ℝ T (ϕ.toFun t x)) = ⊤ ↔ Submodule.span ℝ (tangentConeAt ℝ S x) ⊔ Submodule.span ℝ (tangentConeAt ℝ T x) = ⊤

Transversality propagates along a flow. When the time-t map is differentiable at x and the time-(-t) map at ϕ t x, the tangent spaces of two flow-invariant sets span E at ϕ t x if and only if they span E at x.