Documentation

TauCeti.Geometry.Manifold.ContMDiff.Curve

Smooth curves joining points of a manifold #

A connected C^n manifold is C^n-path connected: any two of its points are joined by a C^n curve γ : ℝ → M which is constant on (-∞, 0] and on [1, ∞) (TauCeti.exists_contMDiff_curve). This holds over every model with corners, so manifolds with boundary or corners are included. Points close to x are joined to x by such curves staying in any prescribed neighbourhood of x (TauCeti.eventually_exists_contMDiff_curve): in the chart at x, follow the segment to the chart point of y, reparametrized by Real.smoothTransition. Mathlib's range I is convex, so the segment stays in the model range.

Curves which are constant near their endpoints can be concatenated smoothly (TauCeti.curveConcat, ContMDiff.curveConcat). The concatenation runs through γ₁ on [0, 1/3] and through γ₂ on [2/3, 1], and rests at the junction point in between, so that it is locally a reparametrization of one of the two curves.

These curves are the test curves of line integrals: a closed 1-form whose integral along every smooth loop vanishes is exact, with primitive the integral along smooth curves from a base point.

Main declarations #

Concatenation of curves #

source
noncomputable def TauCeti.curveConcat {X : Type u_1} (γ₁ γ₂ : ℝ → X) (t : ℝ) :
X

The concatenation of two curves γ₁ γ₂ : ℝ → X: it is γ₁ (3 * t) for t ≤ 1/2 and γ₂ (3 * t - 2) for t > 1/2. On [0, 1] it runs through γ₁ on [0, 1] and then through γ₂ on [0, 1]. When γ₁ is constant on [1, ∞) and γ₂ on (-∞, 0] with the same value, it rests at that point on [1/3, 2/3], so near every parameter it agrees with a reparametrization of γ₁ or of γ₂ (TauCeti.eqOn_curveConcat_left, TauCeti.eqOn_curveConcat_right).

Instances For
    source
    @[simp]
    theorem TauCeti.curveConcat_of_le {X : Type u_1} {γ₁ γ₂ : ℝ → X} {t : ℝ} (ht : t ≤ 2⁻¹) :
    curveConcat γ₁ γ₂ t = γ₁ (3 * t)
    source
    @[simp]
    theorem TauCeti.curveConcat_of_lt {X : Type u_1} {γ₁ γ₂ : ℝ → X} {t : ℝ} (ht : 2⁻¹ < t) :
    curveConcat γ₁ γ₂ t = γ₂ (3 * t - 2)
    source
    theorem TauCeti.eqOn_curveConcat_left {X : Type u_1} {γ₁ γ₂ : ℝ → X} {y : X} (h₁ : ∀ (t : ℝ), 1 ≤ t → γ₁ t = y) (h₂ : ∀ t ≤ 0, γ₂ t = y) :
    Set.EqOn (curveConcat γ₁ γ₂) (fun (t : ℝ) => γ₁ (3 * t)) (Set.Iio (2 / 3))

    If γ₁ rests at y from time 1 on and γ₂ rests at y up to time 0, then the concatenation agrees with γ₁ at triple speed before time 2/3.

    source
    theorem TauCeti.eqOn_curveConcat_right {X : Type u_1} {γ₁ γ₂ : ℝ → X} {y : X} (h₁ : ∀ (t : ℝ), 1 ≤ t → γ₁ t = y) (h₂ : ∀ t ≤ 0, γ₂ t = y) :
    Set.EqOn (curveConcat γ₁ γ₂) (fun (t : ℝ) => γ₂ (3 * t - 2)) (Set.Ioi (1 / 3))

    If γ₁ rests at y from time 1 on and γ₂ rests at y up to time 0, then the concatenation agrees with γ₂ at triple speed, shifted, after time 1/3.

    source
    theorem TauCeti.curveConcat_eq_of_mem_Icc {X : Type u_1} {γ₁ γ₂ : ℝ → X} {t : ℝ} {y : X} (h₁ : ∀ (t : ℝ), 1 ≤ t → γ₁ t = y) (h₂ : ∀ t ≤ 0, γ₂ t = y) (ht : t ∈ Set.Icc (1 / 3) (2 / 3)) :
    curveConcat γ₁ γ₂ t = y

    If γ₁ rests at y from time 1 on and γ₂ rests at y up to time 0, then the concatenation rests at y between times 1/3 and 2/3.

    source
    theorem ContMDiff.curveConcat {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] {n : WithTop ℕ∞} {γ₁ γ₂ : ℝ → M} {y : M} (hγ₁ : ContMDiff (modelWithCornersSelf ℝ ℝ) I n γ₁) (hγ₂ : ContMDiff (modelWithCornersSelf ℝ ℝ) I n γ₂) (h₁ : ∀ (t : ℝ), 1 ≤ t → γ₁ t = y) (h₂ : ∀ t ≤ 0, γ₂ t = y) :
    ContMDiff (modelWithCornersSelf ℝ ℝ) I n (TauCeti.curveConcat γ₁ γ₂)

    The concatenation of two C^n curves, the first resting at y from time 1 on and the second resting at y up to time 0, is C^n.

    Smooth path connectivity #

    source
    theorem TauCeti.eventually_exists_contMDiff_curve {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] {n : ℕ∞} [IsManifold I (↑n) M] {x : M} {U : Set M} (hU : U ∈ nhds x) :
    ∀ᶠ (y : M) in nhds x, ∃ (γ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑n) γ ∧ (∀ t ≤ 0, γ t = x) ∧ (∀ (t : ℝ), 1 ≤ t → γ t = y) ∧ ∀ (t : ℝ), γ t ∈ U

    Points close to x are joined to x by C^n curves staying in a prescribed neighbourhood U of x, which are constant on (-∞, 0] and on [1, ∞).

    source
    theorem TauCeti.exists_contMDiff_curve {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] {n : ℕ∞} [IsManifold I (↑n) M] [PreconnectedSpace M] (x y : M) :
    ∃ (γ : ℝ → M), ContMDiff (modelWithCornersSelf ℝ ℝ) I (↑n) γ ∧ (∀ t ≤ 0, γ t = x) ∧ ∀ (t : ℝ), 1 ≤ t → γ t = y

    Smooth path connectivity. In a preconnected C^n manifold, any two points are joined by a C^n curve γ : ℝ → M which is constant on (-∞, 0] and on [1, ∞).