Monotonicity of functions along integral curves

Let γ be an integral curve of a vector field v on a manifold, and f a real function, differentiable along γ, with df(v) ≤ 0 along γ. Then f never increases along γ. If moreover df(v) < 0 at γ s, then f drops strictly below f (γ s) at every later time, with no further sign condition at the later points.

These are the monotonicity statements behind the deformation of sublevels along descending vector fields, which are allowed to vanish away from the region being deformed.

If instead df(v) = 0 along an integral curve defined on a preconnected set of times, then f is constant along it. This is the conservation statement behind first integrals of a vector field.

If df(v) > 0 is only known at the points of γ on a level f⁻¹(c), then γ crosses that level only upwards: once f (γ a) ≥ c, it stays in {f > c} at every later time, and once f (γ b) ≤ c, it was in {f < c} at every earlier time. This is how the trajectories of a vector field pointing out of a domain {f ≤ c} along its boundary are shown never to re-enter it.

Finally, an integral curve along which the vector field vanishes does not move at all: it is a constant curve.

Main declarations

• IsMIntegralCurve.antitone_comp: f is antitone along γ.
• IsMIntegralCurve.lt_of_mvfderiv_apply_lt_zero: f strictly decreases along γ after a time at which df(v) < 0.
• IsMIntegralCurveOn.apply_eq_of_mvfderiv_apply_eq_zero: f is constant along γ when df(v) = 0 along it.
• IsMIntegralCurveOn.lt_apply_of_le_apply, IsMIntegralCurveOn.apply_lt_of_apply_le: γ crosses a level of f only upwards when df(v) > 0 along that level.
• IsMIntegralCurve.apply_eq_of_forall_eq_zero: an integral curve along which the vector field vanishes is constant.

theorem IsMIntegralCurve.antitone_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {f : M → ℝ} (hγ : IsMIntegralCurve γ v) (hf : ∀ (t : ℝ), MDiffAt f (γ t)) (hvf : ∀ (t : ℝ), (d% f (γ t)) (v (γ t)) ≤ 0) : Antitone (f ∘ γ)

Monotonicity along an integral curve. If f is differentiable along an integral curve γ of v and df(v) ≤ 0 along γ, then f is antitone along γ.

theorem IsMIntegralCurve.lt_of_mvfderiv_apply_lt_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {f : M → ℝ} (hγ : IsMIntegralCurve γ v) (hf : ∀ (t : ℝ), MDiffAt f (γ t)) (hvf : ∀ (t : ℝ), (d% f (γ t)) (v (γ t)) ≤ 0) {s t : ℝ} (hs : (d% f (γ s)) (v (γ s)) < 0) (hst : s < t) : f (γ t) < f (γ s)

Strict decrease along an integral curve. If f is differentiable along an integral curve γ of v, df(v) ≤ 0 along γ and df(v) < 0 at γ s, then f (γ t) < f (γ s) for every t > s.

theorem IsMIntegralCurve.apply_eq_of_forall_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} [IsManifold I 1 M] (hγ : IsMIntegralCurve γ v) (hv : ∀ (t : ℝ), v (γ t) = 0) (s t : ℝ) : γ t = γ s

An integral curve along which the field vanishes is constant. If v (γ t) = 0 for every t, then the integral curve γ of v has zero derivative everywhere, so it is constant.

theorem IsMIntegralCurveOn.apply_eq_of_mvfderiv_apply_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {f : M → ℝ} {s : Set ℝ} (hγ : IsMIntegralCurveOn γ v s) (hs' : IsPreconnected s) (hf : ∀ t ∈ s, MDiffAt f (γ t)) (hvf : ∀ t ∈ s, (d% f (γ t)) (v (γ t)) = 0) {t₀ t : ℝ} (ht₀ : t₀ ∈ s) (ht : t ∈ s) : f (γ t) = f (γ t₀)

Constancy along an integral curve. If f is differentiable along an integral curve γ of v on a preconnected set of times s, such as an interval, and df(v) = 0 along γ on s, then f is constant along γ on s.

theorem IsMIntegralCurveOn.lt_apply_of_le_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {f : M → ℝ} {s : Set ℝ} {c a b : ℝ} (hγ : IsMIntegralCurveOn γ v s) (hs : IsOpen s) (hab : Set.Icc a b ⊆ s) (hf : ContinuousOn (f ∘ γ) (Set.Icc a b)) (hvf : ∀ t ∈ Set.Icc a b, f (γ t) = c → MDiffAt f (γ t) ∧ 0 < (d% f (γ t)) (v (γ t))) (ha : c ≤ f (γ a)) ⦃t : ℝ⦄ : t ∈ Set.Ioc a b → c < f (γ t)

Integral curves cross a level only upwards. Let γ be an integral curve of v on an open set containing [a, b], with f ∘ γ continuous on [a, b], and suppose that f is differentiable with df(v) > 0 at every point γ t, t ∈ [a, b], of the level f⁻¹(c). If c ≤ f (γ a), then c < f (γ t) for every t ∈ (a, b].

theorem IsMIntegralCurveOn.apply_lt_of_apply_le {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {v : (x : M) → TangentSpace I x} {γ : ℝ → M} {f : M → ℝ} {s : Set ℝ} {c a b : ℝ} (hγ : IsMIntegralCurveOn γ v s) (hs : IsOpen s) (hab : Set.Icc a b ⊆ s) (hf : ContinuousOn (f ∘ γ) (Set.Icc a b)) (hvf : ∀ t ∈ Set.Icc a b, f (γ t) = c → MDiffAt f (γ t) ∧ 0 < (d% f (γ t)) (v (γ t))) (hb : f (γ b) ≤ c) ⦃t : ℝ⦄ : t ∈ Set.Ico a b → f (γ t) < c

Integral curves cross a level only upwards, looking backwards. Let γ be an integral curve of v on an open set containing [a, b], with f ∘ γ continuous on [a, b], and suppose that f is differentiable with df(v) > 0 at every point γ t, t ∈ [a, b], of the level f⁻¹(c). If f (γ b) ≤ c, then f (γ t) < c for every t ∈ [a, b).