Differentiating along a curve in a manifold

A curve γ : 𝕜 → M in a manifold has a one-dimensional parameter, so a function on M restricted along it has an honest HasDerivWithinAt derivative rather than only a manifold differential. Mathlib's composition lemmas for mvfderiv are stated for a manifold source, and its deriv composition lemmas for a normed-space source, so neither directly produces that derivative. This file records the resulting chain rule, and the special case of reading the curve in the extended chart centred at the current point, where the derivative is the velocity itself.

Following Mathlib's IsIntegralCurveOn, the velocity w : TangentSpace I (γ t) is presented through HasMFDerivWithinAt 𝓘(𝕜, 𝕜) I γ s t ((1 : 𝕜 →L[𝕜] 𝕜).smulRight w), since TangentSpace 𝓘(𝕜, 𝕜) t carries no One instance and mfderivWithin ... 1 therefore does not elaborate.

The velocity itself is named here: TauCeti.Manifold.curveVelocityWithin reads the derivative within a parameter set on the unit tangent vector, so that a statement about the velocity of a curve need not carry a HasMFDerivWithinAt witness for it.

Main definitions and results

• TauCeti.Manifold.hasDerivWithinAt_comp_curve: the chain rule (g ∘ γ)' (t) = d g (γ t) (γ' t) for a function g from the manifold to a normed space, with TauCeti.Manifold.hasDerivAt_comp_curve its unrestricted case.
• TauCeti.Manifold.curveVelocityWithin and TauCeti.Manifold.curveVelocity: the velocity of a curve within a parameter set and its unrestricted case, computed by TauCeti.Manifold.curveVelocityWithin_apply and TauCeti.Manifold.curveVelocity_apply and related by TauCeti.Manifold.curveVelocityWithin_univ; for a curve in a normed space they are its derivatives (TauCeti.Manifold.curveVelocityWithin_eq_derivWithin).
• TauCeti.Manifold.curveVelocityLiftWithin and TauCeti.Manifold.curveVelocityLift: the corresponding curves in the tangent bundle, together with their projection and fibre formulas.
• TauCeti.Manifold.tangentMap_curveVelocityLiftWithin: tangent maps carry velocity lifts to velocity lifts, with TauCeti.Manifold.tangentMap_curveVelocityLift as its unrestricted form.
• ContMDiffOn.continuousOn_curveVelocityLiftWithin: the within-domain velocity lift of a C¹ curve is continuous on a unique-differentiability domain, with open-domain and unrestricted forms for curveVelocityLift.
• TauCeti.Manifold.hasMFDerivWithinAt_curveVelocityWithin and TauCeti.Manifold.curveVelocityWithin_eq_of_hasMFDerivWithinAt: the two directions relating the named velocity to a HasMFDerivWithinAt witness.
• TauCeti.Manifold.curveVelocityWithin_subset and TauCeti.Manifold.curveVelocityWithin_comp: velocity is unchanged by restriction and obeys the chain rule under reparametrization, with MDifferentiableAt.curveVelocity_comp_mfderiv for a curve through a normed space and TauCeti.Manifold.curveVelocity_comp for scalar reparametrizations.
• TauCeti.Manifold.curveVelocity_eq_mfderiv_snd and TauCeti.Manifold.curveVelocity_eq_mfderiv_fst: the two partial velocities of a two-parameter family f : 𝕜 → 𝕜 → M are the differential of the uncurried family in the coordinate directions.
• TauCeti.Manifold.variationField: the variation field V(t) = ∂F/∂s (0, t) of a two-parameter family F : 𝕜 → 𝕜 → M, the transverse velocity at s = 0; it vanishes where the curves near s = 0 share a point (TauCeti.Manifold.variationField_eq_zero) and is the differential of the uncurried family in the first coordinate direction (TauCeti.Manifold.variationField_eq_mfderiv).
• TauCeti.Manifold.hasDerivWithinAt_extChartAt_comp_curve: reading the curve in the chart centred at the current point differentiates it to the velocity itself, with TauCeti.Manifold.hasDerivAt_extChartAt_comp_curve its unrestricted case and TauCeti.Manifold.derivWithin_extChartAt_comp_curve its form for the named velocity.

theorem TauCeti.Manifold.hasDerivWithinAt_comp_curve {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} {g : M → F} (hg : MDiffAt g (γ t)) (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) : HasDerivWithinAt (g ∘ γ) ((d% g (γ t)) w) s t

The chain rule along a curve. If g is a normed-space-valued function which is differentiable at γ t, and the curve γ has velocity w at t within the parameter set s, then g ∘ γ has derivative d g (γ t) w there. The velocity is presented as in Mathlib's integral-curve API, as the value of the manifold derivative on the unit tangent vector.

theorem TauCeti.Manifold.hasDerivAt_comp_curve {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {γ : 𝕜 → M} {t : 𝕜} {w : TangentSpace I (γ t)} {g : M → F} (hg : MDiffAt g (γ t)) (hγ : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 w)) : HasDerivAt (g ∘ γ) ((d% g (γ t)) w) t

The unrestricted case of TauCeti.Manifold.hasDerivWithinAt_comp_curve.

The velocity of a curve

noncomputable def TauCeti.Manifold.curveVelocityWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (s : Set 𝕜) (t : 𝕜) : TangentSpace I (γ t)

The velocity of the curve γ at the parameter t, taken within the parameter set s: the value at the unit tangent vector of the manifold derivative of γ within s. Where γ is not differentiable within s at t, this carries Mathlib's junk value 0; where the derivative within s is not unique it need not be the velocity of any parametrization.

Equations

• TauCeti.Manifold.curveVelocityWithin I γ s t = (mfderiv[s] γ t) 1

noncomputable def TauCeti.Manifold.curveVelocity {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (t : 𝕜) : TangentSpace I (γ t)

The velocity of the curve γ at the parameter t, with unrestricted derivative. This is the s = Set.univ case of TauCeti.Manifold.curveVelocityWithin.

Equations

• TauCeti.Manifold.curveVelocity I γ t = TauCeti.Manifold.curveVelocityWithin I γ Set.univ t

@[simp]

theorem TauCeti.Manifold.curveVelocityWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} : curveVelocityWithin I γ Set.univ = curveVelocity I γ

theorem TauCeti.Manifold.curveVelocityWithin_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} : curveVelocityWithin I γ s t = (mfderiv[s] γ t) 1

The velocity within s is the derivative within s evaluated at the unit tangent vector. This restates the definition, whose body is not exposed across the module boundary.

theorem TauCeti.Manifold.curveVelocity_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {t : 𝕜} : curveVelocity I γ t = (mfderiv% γ t) 1

The unrestricted velocity is the unrestricted derivative evaluated at the unit tangent vector.

theorem TauCeti.Manifold.curveVelocityWithin_map {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} (hf : MDiffAt f (γ t)) (hs : UniqueDiffWithinAt 𝕜 s t) (hγ : MDiffAt[s] γ t) : curveVelocityWithin J (f ∘ γ) s t = (mfderiv% f (γ t)) (curveVelocityWithin I γ s t)

The velocity of the image of a curve under a differentiable map is the differential of the map applied to the velocity of the curve. The derivative within the parameter set is uniquely determined at t.

theorem TauCeti.Manifold.hasMFDerivWithinAt_curveVelocityWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} (hγ : MDiffAt[s] γ t) : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 (curveVelocityWithin I γ s t))

A curve differentiable within s at t has TauCeti.Manifold.curveVelocityWithin as its velocity there.

theorem TauCeti.Manifold.hasMFDerivAt_curveVelocity {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {t : 𝕜} (hγ : MDiffAt γ t) : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (curveVelocity I γ t))

The unrestricted case of TauCeti.Manifold.hasMFDerivWithinAt_curveVelocityWithin.

theorem TauCeti.Manifold.curveVelocityWithin_eq_of_hasMFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) (hs : UniqueDiffWithinAt 𝕜 s t) : curveVelocityWithin I γ s t = w

A velocity witnessed by a HasMFDerivWithinAt statement is the velocity, as soon as the derivative within the parameter set is unique.

theorem TauCeti.Manifold.curveVelocityWithin_subset {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {u : Set 𝕜} (hus : u ⊆ s) (hu : UniqueDiffWithinAt 𝕜 u t) (hγ : MDiffAt[s] γ t) : curveVelocityWithin I γ u t = curveVelocityWithin I γ s t

Restricting the parameter set does not change the velocity of a differentiable curve when the smaller set has a unique derivative at the parameter.

theorem MDifferentiableAt.curveVelocity_comp_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : 𝕜} {f : F → M} {g : 𝕜 → F} {w : F} (hf : MDiffAt f (g t)) (hg : HasDerivAt g w t) : TauCeti.Manifold.curveVelocity I (f ∘ g) t = (mfderiv% f (g t)) w

The manifold chain rule for the velocity of a curve. If g is a curve through a normed space with velocity w, then the velocity of f ∘ g is the manifold differential of f applied to w.

theorem TauCeti.Manifold.curveVelocity_eq_mfderiv_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {t : 𝕜} {f : 𝕜 → 𝕜 → M} {u : 𝕜} (hf : (MDiffAt fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, t)) : curveVelocity I (f u) t = ((mfderiv% fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, t)) (0, 1)

The velocity of a curve of a two-parameter family. The velocity of the curve f u of a family f : 𝕜 → 𝕜 → M is the differential of the uncurried family in the direction of the second parameter.

theorem TauCeti.Manifold.curveVelocity_eq_mfderiv_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {t : 𝕜} {f : 𝕜 → 𝕜 → M} {u : 𝕜} (hf : (MDiffAt fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, t)) : curveVelocity I (fun (q : 𝕜) => f q t) u = ((mfderiv% fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, t)) (1, 0)

The transverse velocity of a two-parameter family. The velocity of the curve q ↦ f q t of a family f : 𝕜 → 𝕜 → M is the differential of the uncurried family in the direction of the first parameter.

theorem TauCeti.Manifold.curveVelocityWithin_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {φ : 𝕜 → 𝕜} {u : Set 𝕜} {c : 𝕜} (hφ : HasDerivWithinAt φ c u t) (hmaps : Set.MapsTo φ u s) (hγ : MDiffAt[s] γ (φ t)) (hu : UniqueDiffWithinAt 𝕜 u t) : curveVelocityWithin I (γ ∘ φ) u t = c • curveVelocityWithin I γ s (φ t)

The velocity of a reparametrized curve is the velocity of the original curve multiplied by the derivative of the reparametrization.

theorem TauCeti.Manifold.curveVelocity_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {t : 𝕜} {φ : 𝕜 → 𝕜} {c : 𝕜} (hφ : HasDerivAt φ c t) (hγ : MDiffAt γ (φ t)) : curveVelocity I (γ ∘ φ) t = c • curveVelocity I γ (φ t)

The velocity of a reparametrized curve is the velocity of the original curve multiplied by the derivative of the reparametrization.

theorem TauCeti.Manifold.curveVelocityWithin_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} (hs : s ∈ nhds t) : curveVelocityWithin I γ s t = curveVelocity I γ t

On a parameter set which is a neighbourhood of t, the restricted velocity is the unrestricted one.

@[simp]

theorem TauCeti.Manifold.curveVelocityWithin_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set 𝕜} {t : 𝕜} (x : M) : curveVelocityWithin I (fun (x_1 : 𝕜) => x) s t = 0

A constant curve has zero velocity within any parameter set.

@[simp]

theorem TauCeti.Manifold.curveVelocity_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {t : 𝕜} (x : M) : curveVelocity I (fun (x_1 : 𝕜) => x) t = 0

A constant curve has zero velocity. This is the unrestricted case of TauCeti.Manifold.curveVelocityWithin_const, which TauCeti.Manifold.curveVelocityWithin_univ would otherwise keep simp from reaching.

@[simp]

theorem TauCeti.Manifold.curveVelocityWithin_eq_derivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set 𝕜} {t : 𝕜} {γ : 𝕜 → F} : curveVelocityWithin (modelWithCornersSelf 𝕜 F) γ s t = derivWithin γ s t

The velocity within s of a curve in a normed space, read in its own model, is its derivative within s.

@[simp]

theorem TauCeti.Manifold.curveVelocity_eq_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t : 𝕜} {γ : 𝕜 → F} : curveVelocity (modelWithCornersSelf 𝕜 F) γ t = deriv γ t

The velocity of a curve in a normed space, read in its own model, is its derivative.

The variation field of a two-parameter family

noncomputable def TauCeti.Manifold.variationField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : 𝕜 → 𝕜 → M) (t : 𝕜) : TangentSpace I (F 0 t)

The variation field of a two-parameter family F : 𝕜 → 𝕜 → M: the velocity at s = 0 of the transverse curve s ↦ F s t, a tangent vector at F 0 t. In the classical notation it is V(t) = ∂F/∂s (0, t).

Equations

• TauCeti.Manifold.variationField I F t = TauCeti.Manifold.curveVelocity I (fun (s : 𝕜) => F s t) 0

theorem TauCeti.Manifold.variationField_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : 𝕜 → 𝕜 → M) (t : 𝕜) : variationField I F t = curveVelocity I (fun (s : 𝕜) => F s t) 0

The defining formula for the variation field.

theorem TauCeti.Manifold.variationField_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (F : 𝕜 → 𝕜 → M) : variationField I F = fun (t : 𝕜) => curveVelocity I (fun (s : 𝕜) => F s t) 0

The variation field as a function of the curve parameter: the unapplied form of variationField_apply.

@[simp]

theorem TauCeti.Manifold.variationField_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : 𝕜 → 𝕜 → M} {t : 𝕜} (h : ∀ᶠ (s : 𝕜) in nhds 0, F s t = F 0 t) : variationField I F t = 0

At a parameter where the curves of the family near s = 0 all pass through the same point, the variation field vanishes.

theorem TauCeti.Manifold.variationField_eq_mfderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {F : 𝕜 → 𝕜 → M} {t : 𝕜} (hf : (MDiffAt fun (z : 𝕜 × 𝕜) => F z.1 z.2) (0, t)) : variationField I F t = ((mfderiv% fun (z : 𝕜 × 𝕜) => F z.1 z.2) (0, t)) (1, 0)

The variation field is the differential of the uncurried family in the direction of the first parameter.

The velocity lift of a curve

noncomputable def TauCeti.Manifold.curveVelocityLiftWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (s : Set 𝕜) (t : 𝕜) : TangentBundle I M

The velocity lift of a curve to the tangent bundle: the curve t ↦ (γ t, γ' t), with the velocity taken within the parameter set s. It inherits the junk values of TauCeti.Manifold.curveVelocityWithin where γ is not differentiable within s.

Equations

• TauCeti.Manifold.curveVelocityLiftWithin I γ s t = ⟨γ t, TauCeti.Manifold.curveVelocityWithin I γ s t⟩

noncomputable def TauCeti.Manifold.curveVelocityLift {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) : 𝕜 → TangentBundle I M

The velocity lift of a curve, with unrestricted velocity. This is the s = Set.univ case of TauCeti.Manifold.curveVelocityLiftWithin.

Equations

• TauCeti.Manifold.curveVelocityLift I γ = TauCeti.Manifold.curveVelocityLiftWithin I γ Set.univ

theorem TauCeti.Manifold.curveVelocityLiftWithin_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (s : Set 𝕜) (t : 𝕜) : curveVelocityLiftWithin I γ s t = ⟨γ t, curveVelocityWithin I γ s t⟩

The defining formula for the velocity lift.

theorem TauCeti.Manifold.curveVelocityLift_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (t : 𝕜) : curveVelocityLift I γ t = ⟨γ t, curveVelocity I γ t⟩

The defining formula for the unrestricted velocity lift.

@[simp]

theorem TauCeti.Manifold.curveVelocityLiftWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) : curveVelocityLiftWithin I γ Set.univ = curveVelocityLift I γ

The velocity lift taken within the whole parameter space is the unrestricted lift.

@[simp]

theorem TauCeti.Manifold.curveVelocityLiftWithin_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (s : Set 𝕜) (t : 𝕜) : (curveVelocityLiftWithin I γ s t).proj = γ t

The velocity lift lies over the curve.

@[simp]

theorem TauCeti.Manifold.curveVelocityLiftWithin_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (s : Set 𝕜) (t : 𝕜) : (curveVelocityLiftWithin I γ s t).snd = curveVelocityWithin I γ s t

The fibre component of the velocity lift is the velocity of the curve.

@[simp]

theorem TauCeti.Manifold.curveVelocityLift_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (t : 𝕜) : (curveVelocityLift I γ t).proj = γ t

The unrestricted velocity lift lies over the curve.

@[simp]

theorem TauCeti.Manifold.curveVelocityLift_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (γ : 𝕜 → M) (t : 𝕜) : (curveVelocityLift I γ t).snd = curveVelocity I γ t

The fibre component of the unrestricted velocity lift is the velocity of the curve.

theorem TauCeti.Manifold.tangentMapWithin_unit_eq_curveVelocityLiftWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {u : Set 𝕜} (t : 𝕜) : tangentMapWithin (modelWithCornersSelf 𝕜 𝕜) I γ u ⟨t, (NormedSpace.fromTangentSpace t).symm 1⟩ = curveVelocityLiftWithin I γ u t

Applying the tangent map of a curve to the canonical unit tangent vector of its parameter space gives its velocity lift.

theorem TauCeti.Manifold.tangentMap_curveVelocityLiftWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {t : 𝕜} {G : Type u_6} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 G H'} {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} {u : Set 𝕜} (hf : MDiffAt f (γ t)) (hγ : MDiffAt[u] γ t) (hu : UniqueMDiffAt[u] t) : tangentMap I J f (curveVelocityLiftWithin I γ u t) = curveVelocityLiftWithin J (f ∘ γ) u t

Tangent maps carry the velocity lift within a parameter set to the velocity lift of the image curve. This is the tangent-bundle form of the within-domain chain rule.

theorem TauCeti.Manifold.tangentMap_curveVelocityLift {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {t : 𝕜} {G : Type u_6} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H' : Type u_7} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 G H'} {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] {f : M → N} (hf : MDiffAt f (γ t)) (hγ : MDiffAt γ t) : tangentMap I J f (curveVelocityLift I γ t) = curveVelocityLift J (f ∘ γ) t

Tangent maps carry the unrestricted velocity lift of a differentiable curve to the velocity lift of its image.

theorem TauCeti.Manifold.ContMDiffOn.continuousOn_curveVelocityLiftWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} [IsManifold I 1 M] {u : Set 𝕜} (hγ : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I 1 γ u) (hu : UniqueMDiff[u]) : ContinuousOn (curveVelocityLiftWithin I γ u) u

The within-domain velocity lift of a C¹ curve is continuous on a domain with unique manifold derivatives.

theorem TauCeti.Manifold.ContMDiffOn.continuousOn_curveVelocityLift {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} [IsManifold I 1 M] {u : Set 𝕜} (hγ : ContMDiffOn (modelWithCornersSelf 𝕜 𝕜) I 1 γ u) (hu : IsOpen u) : ContinuousOn (curveVelocityLift I γ) u

The velocity lift of a C¹ curve is continuous on an open parameter set. The openness ensures that the unrestricted velocity in curveVelocityLift agrees with the derivative within the parameter set.

theorem TauCeti.Manifold.ContMDiff.continuous_curveVelocityLift {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} [IsManifold I 1 M] (hγ : ContMDiff (modelWithCornersSelf 𝕜 𝕜) I 1 γ) : Continuous (curveVelocityLift I γ)

The unrestricted case of ContMDiffOn.continuousOn_curveVelocityLift.

theorem TauCeti.Manifold.hasDerivWithinAt_extChartAt_comp_curve {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} {w : TangentSpace I (γ t)} [IsManifold I 1 M] (hγ : HasMFDerivAt[s] γ t (ContinuousLinearMap.smulRight 1 w)) : HasDerivWithinAt (↑(extChartAt I (γ t)) ∘ γ) w s t

Reading the curve in the extended chart centred at the current point differentiates it to the velocity itself: the derivative of that chart at its own centre is the identity.

theorem TauCeti.Manifold.hasDerivAt_extChartAt_comp_curve {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {t : 𝕜} {w : TangentSpace I (γ t)} [IsManifold I 1 M] (hγ : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 w)) : HasDerivAt (↑(extChartAt I (γ t)) ∘ γ) w t

The unrestricted case of TauCeti.Manifold.hasDerivWithinAt_extChartAt_comp_curve.

theorem TauCeti.Manifold.derivWithin_extChartAt_comp_curve {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {γ : 𝕜 → M} {s : Set 𝕜} {t : 𝕜} [IsManifold I 1 M] (hγ : MDiffAt[s] γ t) (hs : UniqueDiffWithinAt 𝕜 s t) : derivWithin (↑(extChartAt I (γ t)) ∘ γ) s t = curveVelocityWithin I γ s t

The derivative within s of a differentiable curve read in the chart centred at the current point is its velocity within s.