IsIntegralCurve.periodic_of_eq
theorem IsIntegralCurve.periodic_of_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x}
[inst_6 : T2Space M] {a b : ℝ} [inst_7 : BoundarylessManifold I M],
IsIntegralCurve γ v →
(ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }) → γ a = γ b → Function.Periodic γ (a - b)
This theorem states that for a global integral curve `γ` in a boundaryless manifold `M`, if it crosses itself at real numbers `a` and `b`, then it is periodic with period `a - b`. Here, `M` is a smooth manifold with corners equipped with a model `I` and charted space `H`. The integral curve `γ` is associated with a vector field `v`. The premise includes the condition that `γ` is a continuously differentiable (once) function from the tangent bundle to the tangent space at each point, with projection `x` and vector `v x`. The topology of `M` is such that no two distinct points can be separated by disjoint open neighborhoods, as indicated by `T2Space M`.
More concisely: If `γ` is a continuously differentiable global integral curve in a boundaryless, T2 manifold `M` with vector field `v`, then `γ` is periodic with period `a - b` whenever it self-intersects at real numbers `a` and `b`.
|
IsIntegralCurve.periodic_xor_injective
theorem IsIntegralCurve.periodic_xor_injective :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x}
[inst_6 : T2Space M] [inst_7 : BoundarylessManifold I M],
IsIntegralCurve γ v →
(ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }) →
Xor' (∃ T > 0, Function.Periodic γ T) (Function.Injective γ)
The theorem `IsIntegralCurve.periodic_xor_injective` states that for a given integral curve `γ` in a boundaryless manifold `M` with a model `I` in a normed space `E`, and a tangent vector field `v`, the curve `γ` is either injective or periodic with a positive period, but not both. More specifically, the property of being injective or periodic with positive period is exclusive, meaning that if `γ` is injective, it is not periodic with positive period, and vice versa. The proof of this statement is omitted here.
More concisely: A given integral curve in a boundaryless manifold with a model in a normed space is either injective or periodic with a positive period, but cannot be both.
|
isIntegralCurveAt_eventuallyEq_of_contMDiffAt
theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ γ' : ℝ → M}
{v : (x : M) → TangentSpace I x} {t₀ : ℝ},
I.IsInteriorPoint (γ t₀) →
ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) (γ t₀) →
IsIntegralCurveAt γ v t₀ → IsIntegralCurveAt γ' v t₀ → γ t₀ = γ' t₀ → (nhds t₀).EventuallyEq γ γ'
This theorem states that local integral curves are unique. Given a continuously differentiable (C¹) vector field `v`, if there exist two local integral curves `γ` and `γ'`, both being functions from real numbers to a manifold `M`, that are both at a point `t₀` such that `γ t₀ = γ' t₀`, then the curves `γ` and `γ'` are the same on some open interval around `t₀`. The conditions for this are that the point `t₀` is an interior point of the curve `γ`, the function mapping `x` to the pair of `x` and `v x` is continuously differentiable at `γ t₀`, and that both `γ` and `γ'` are integral curves of `v` at `t₀`.
More concisely: Given a continuously differentiable vector field `v` on a manifold `M`, if two local integral curves `γ` and `γ'` of `v` intersect at an interior point `t₀` and the function mapping `x` to `(x, v x)` is continuously differentiable at `γ t₀`, then `γ` and `γ'` coincide on some open interval around `t₀`.
|
isIntegralCurveOn_Ioo_eqOn_of_contMDiff
theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ γ' : ℝ → M}
{v : (x : M) → TangentSpace I x} {t₀ : ℝ} [inst_6 : T2Space M] {a b : ℝ},
t₀ ∈ Set.Ioo a b →
(∀ t ∈ Set.Ioo a b, I.IsInteriorPoint (γ t)) →
(ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }) →
IsIntegralCurveOn γ v (Set.Ioo a b) →
IsIntegralCurveOn γ' v (Set.Ioo a b) → γ t₀ = γ' t₀ → Set.EqOn γ γ' (Set.Ioo a b)
This theorem states that the integral curves of a continuously differentiable vector field `v` are unique on open intervals. More specifically, if we have two integral curves `γ` and `γ'` for the vector field `v` on the open interval between `a` and `b`, and if for some `t` within this interval, the values `γ t₀` and `γ' t₀` coincide, then these two curves are identical on the entire interval. This is applicable in a smooth manifold with corners `M`, equipped with a model with corners `I` from the normed space `E` to the topological space `H`. It assumes that `M` is a T2 space (a topological space where any two distinct points have disjoint open neighborhoods).
More concisely: Given a continuously differentiable vector field `v` on an open interval in a T2 topological space `M` with corners, if any two integral curves `γ` and `γ'` of `v` on this interval have a point in common, then they are equal on the entire interval.
|
isIntegralCurve_const
theorem isIntegralCurve_const :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {v : (x : M) → TangentSpace I x} {x : M},
v x = 0 → IsIntegralCurve (fun x_1 => x) v
This theorem states that for any vector field `v` in a smooth manifold `M` with a chosen model of corners `I`, if `v` is zero at a certain point `x`, then the constant curve at `x` is a global integral curve of `v`. Here, `x` belongs to the tangent space at `x` in the manifold `M`. The tangent space is a vector space at `x` that contains all possible directions in which one can "tangentially" move away from `x` in the manifold. An integral curve of a vector field is a curve that is "aligned" with the vectors of the field at each point.
More concisely: If a vector field on a smooth manifold is zero at a point, then the constant curve at that point is a global integral curve of the vector field in the manifold's tangent space.
|
exists_isIntegralCurveAt_of_contMDiffAt_boundaryless
theorem exists_isIntegralCurveAt_of_contMDiffAt_boundaryless :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {H : Type u_2}
[inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_4 : TopologicalSpace M]
[inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M] {v : (x : M) → TangentSpace I x} (t₀ : ℝ)
{x₀ : M} [inst_7 : BoundarylessManifold I M],
ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) x₀ → ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀
The theorem `exists_isIntegralCurveAt_of_contMDiffAt_boundaryless` states that for any $C^1$ vector field `v` on a smooth manifold `M` without boundary, if the vector field is continuously differentiable at a point `x₀`, then there exists a local integral curve `γ` at `t₀` such that `γ(t₀) = x₀` and `γ` is an integral curve of `v` at `t₀`. Here, `E` represents a normed add commutative group, `H` represents a topological space, and `I` is a model with corners. Various other conditions regarding the topological and differential structures on the manifold are also assumed.
More concisely: Given a smooth manifold without boundary `M` and a $C^1$ vector field `v` on `M` that is continuously differentiable at a point `x₀`, there exists a local integral curve `γ` of `v` passing through `x₀`.
|
isIntegralCurve_eq_of_contMDiff
theorem isIntegralCurve_eq_of_contMDiff :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ γ' : ℝ → M}
{v : (x : M) → TangentSpace I x} {t₀ : ℝ} [inst_6 : T2Space M],
(∀ (t : ℝ), I.IsInteriorPoint (γ t)) →
(ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }) →
IsIntegralCurve γ v → IsIntegralCurve γ' v → γ t₀ = γ' t₀ → γ = γ'
The theorem `isIntegralCurve_eq_of_contMDiff` states that given a continuously differentiable vector field `v` on a smooth manifold `M` with a model `I`, if there are two global integral curves `γ` and `γ'` from real numbers to `M`, and for some real number `t₀`, `γ t₀` equals `γ' t₀`, then these two curves are identical. This theorem is under the condition that each point on the curve `γ` is an interior point of `I`, and the mapping from each point in the tangent space to its projection and applied vector field `v` is continuously differentiable. The underlying space `M` is Hausdorff.
More concisely: Given a continuously differentiable vector field on a smooth manifold with the stated properties, if two integral curves have the same value at some point and each point on one curve is an interior point, then they are equal.
|
isIntegralCurveAt_iff'
theorem isIntegralCurveAt_iff' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x}
{t₀ : ℝ}, IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
This theorem states that a function `γ` is an integral curve for a vector field `v` at a specific time `t₀` if and only if `γ` is an integral curve on some interval around `t₀`. More specifically, `γ` being an integral curve at `t₀` is equivalent to the existence of a positive real number `ε` such that `γ` is an integral curve on the set of all points `t` whose distance from `t₀` is less than `ε` (denoted as `Metric.ball t₀ ε`). Here, the types `E`, `H`, `M`, and `I` represent a normed additive commutative group, a topological space, another topological space endowed with a chart structure, and a model with corners (a mathematical structure used to describe manifolds with boundary), respectively.
More concisely: A function `γ : I -> E` is an integral curve of a vector field `v : M ->Vector E` at `t₀ ∈ I` if and only if there exists a positive real number `ε` such that `γ` restricts to an integral curve on the open ball `Metric.ball t₀ ε` in `I`.
|
IsIntegralCurveAt.isIntegralCurveOn
theorem IsIntegralCurveAt.isIntegralCurveOn :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x}
{s : Set ℝ}, (∀ t ∈ s, IsIntegralCurveAt γ v t) → IsIntegralCurveOn γ v s
The theorem `IsIntegralCurveAt.isIntegralCurveOn` states that if a function `γ` is an integral curve at every point `t` in a set `s` of real numbers, then `γ` is an integral curve on the set `s`. Here, `E` is a normed add commutative group, `H` is a topological space, `I` is a model with corners in `E` and `H`, `M` is another topological space which is a charted space in `H` with smooth manifold with corners `I`. `γ` is a function from real numbers to `M`, `v` is a function from `M` to the tangent space at `I` of `M`. The integral curve is in the context of differential geometry.
More concisely: If a curve `γ : ℝ → M` in a charted space `M` over a model `I` with smooth manifold with corners in `E × H`, and `v` is the velocity function, is an integral curve at every point in a set `s ⊆ ℝ`, then `γ` is an integral curve on `s`.
|
IsIntegralCurveOn.hasDerivAt
theorem IsIntegralCurveOn.hasDerivAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x}
{s : Set ℝ} {t₀ : ℝ},
IsIntegralCurveOn γ v s →
∀ {t : ℝ},
t ∈ s →
γ t ∈ (extChartAt I (γ t₀)).source →
HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
This theorem states that if `γ` is an integral curve of a vector field `v`, then the derivative of `γ` at a point `t`, when evaluated in a local chart around the initial point `γ t₀`, is equal to the tangent vector of `v` at the point `γ t`. Here, `s` is a set of real numbers, `t₀` is a real number, `M` is a topological space, `I` is a model with corners, `H` is another topological space, and `E` is a normed additive commutative group with a real vector space structure. This theorem holds under the assumption that `γ` is an integral curve on `v` over the set `s`, `t` is in `s`, and `γ t` lies in the source of the exterior chart at `γ t₀`. The term "integral curve" refers to a curve that is everywhere tangent to a given vector field, and "tangent vector" is a vector that touches and points in the direction of the curve.
More concisely: The derivative of an integral curve `γ` of a vector field `v` at a point `t` in its domain, evaluated in a local chart around `γ t₀`, is equal to the tangent vector of `v` at `γ t`.
|
exists_isIntegralCurveAt_of_contMDiffAt
theorem exists_isIntegralCurveAt_of_contMDiffAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {H : Type u_2}
[inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_4 : TopologicalSpace M]
[inst_5 : ChartedSpace H M] [inst_6 : SmoothManifoldWithCorners I M] {v : (x : M) → TangentSpace I x} (t₀ : ℝ)
{x₀ : M},
ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) x₀ →
I.IsInteriorPoint x₀ → ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀
This theorem asserts the existence of local integral curves for a $C^1$ vector field at interior points on a smooth manifold. Given a smooth manifold with a $C^1$ vector field, if the vector field is continuously differentiable at a particular interior point, then there exists a curve on the manifold that is an integral curve of the vector field at that point. This means the curve's derivative at that point equals the vector field at the same point.
More concisely: Given a smooth manifold with a $C^1$ vector field and a point on the manifold where the vector field is $C^1$, there exists an integral curve of the vector field passing through that point.
|
isIntegralCurveAt_iff
theorem isIntegralCurveAt_iff :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2}
[inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M]
[inst_4 : ChartedSpace H M] [inst_5 : SmoothManifoldWithCorners I M] {γ : ℝ → M} {v : (x : M) → TangentSpace I x}
{t₀ : ℝ}, IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ nhds t₀, IsIntegralCurveOn γ v s
The theorem `isIntegralCurveAt_iff` states that for all real-valued functions `γ` and tangent vectors `v` at a point `t₀` in a smooth manifold `M` with corners associated with a model `I`, the function `γ` is an integral curve at `t₀` if and only if there exists a set `s` that is a neighborhood of `t₀` such that `γ` is an integral curve on `s`. This holds in a normed add commutative group `E` over the reals with a normed space structure, a topological space `H`, and a charted space structure on `M` over `H`.
More concisely: A real-valued function γ on a smooth manifold M with corners is an integral curve at a point t₀ if and only if there exists a neighborhood s of t₀ such that γ restricts to an integral curve on s.
|