SmoothIntegralCurve.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth integral curves on a smooth manifold without boundary

theorem OAI.PolycyclicRecognition.contMDiffAt_chart_velocity line 21

Source documentation

A smooth vector field pushed into a vector-space chart is smooth.

theorem contMDiffAt_chart_velocity
    {φ : M → E} {v : (x : M) → TangentSpace (𝓘(ℝ, E)) x} {x₀ : M}
    (hφ : ContMDiffAt (𝓘(ℝ, E)) (𝓘(ℝ, E)) ∞ φ x₀)
    (hv : ContMDiffAt (𝓘(ℝ, E)) ((𝓘(ℝ, E)).prod (𝓘(ℝ, E))) ∞
      (fun x => (⟨x, v x⟩ : TangentBundle (𝓘(ℝ, E)) M)) x₀) :
    ContMDiffAt (𝓘(ℝ, E)) (𝓘(ℝ, E)) ∞
      (fun x => (mfderiv (𝓘(ℝ, E)) (𝓘(ℝ, E)) φ x) (v x)) x₀ := by
…

theorem OAI.PolycyclicRecognition.IsMIntegralCurve.contMDiff line 34
Source documentation
Smoothness of a vector field upgrades its integral curves from the defining first derivative to all finite derivatives.
```
theorem IsMIntegralCurve.contMDiff
    {γ : ℝ → M} {v : (x : M) → TangentSpace (𝓘(ℝ, E)) x}
    (hγ : IsMIntegralCurve (I := 𝓘(ℝ, E)) γ v)
…
```