structure SmoothFlow (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] : Type u_1

A smooth flow $\varphi_t : M \to M$ on a smooth $n$-manifold $M$: a time-parameterized family of smooth self-maps with $\varphi_0 = \mathrm{id}_M$.

• toFun : ℝ → M → M
• map_zero (x : M) : self.toFun 0 x = x
• smooth (t : ℝ) : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ (self.toFun t)

@[simp]

theorem SmoothFlow.toFun_zero {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] (φ : SmoothFlow n M) (x : M) : φ.toFun 0 x = x

The flow at time $t = 0$ is the identity: $\varphi_0(x) = x$.

structure SmoothIsotopy (n : ℕ) (M : Type u_1) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] extends SmoothFlow n M : Type u_1

A smooth isotopy: a smooth flow $\varphi_t : M \to M$ whose evaluation map $(t, x) \mapsto \varphi_t(x)$ is jointly smooth on $\mathbb{R} \times M$.

• toFun : ℝ → M → M
• map_zero (x : M) : self.toFun 0 x = x
• smooth (t : ℝ) : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ (self.toFun t)
• jointly_smooth : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n)))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ fun (p : ℝ × M) => self.toFun p.1 p.2

noncomputable def SmoothFlow.ofVectorField {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] [CompactSpace M] (X : ℝ → (x : M) → TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n)))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).tangent ⊤ fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) : SmoothFlow n M

Existence of a smooth flow generated by a (time-dependent) vector field $X_t$ on a compact smooth manifold $M$: the global flow $\varphi_t$ obtained by integrating $X$.

theorem SmoothFlow.ofVectorField_ode {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ M] [CompactSpace M] (X : ℝ → (x : M) → TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n)))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).tangent ⊤ fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) : have φ := (ofVectorField X hX).toFun; ∀ (t : ℝ) (x : M), HasMFDerivAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (fun (s : ℝ) => φ s x) t (ContinuousLinearMap.smulRight 1 (X t (φ t x)))

The flow generated by $X$ satisfies the ODE $\frac{d}{dt}\varphi_t(x) = X_t(\varphi_t(x))$, i.e. its time derivative equals $X$ evaluated along the integral curve.