7.4. Path.CotangentCoeff🔗

Jacobians.Path.CotangentCoeff — source

continuousAt_inCoordinates

The continuous local object. Near x₀, the coordinate of the section α in the FIXED hom-bundle trivialization at x₀ is continuous (indeed it is ContMDiffAt) as a map into the fixed normed space ℂ →L[ℂ] ℂ. This is inCoordinates (α x).

theorem continuousAt_inCoordinates {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X) (x₀ : X)
    :
    ContinuousAt (fun x : X => ContinuousLinearMap.inCoordinates ℂ
      (TangentSpace 𝓘(ℂ) (M := X)) ℂ (Bundle.Trivial X ℂ) x₀ x x₀ x (α.toFun x)) x₀

continuousAt_localCoeff

The local coefficient is continuous. x ↦ inCoordinates (α x) 1 (the coefficient of α read in the FIXED chart at x₀, i.e. α paired with the *coordinate vector field of the chart at x₀*) is continuous at x₀. NOTE this is inCoordinates (α x) 1, not the discontinuous α x 1.

theorem continuousAt_localCoeff {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X) (x₀ : X)
    :
    ContinuousAt (fun x : X => ContinuousLinearMap.inCoordinates ℂ
      (TangentSpace 𝓘(ℂ) (M := X)) ℂ (Bundle.Trivial X ℂ) x₀ x x₀ x (α.toFun x) (1 : ℂ)) x₀

apply_eq_inCoordinates

General-vector form of target_eq_inCoordinates_of_w. For any tangent vector v at x ∈ (chartAt ℂ x₀).source, applying the form equals applying its fixed-x₀-trivialization inCoordinates representation to v read in that trivialization. (The v = 1 case is the obstruction lemma target_eq_inCoordinates_of_w; this general version is what lets a chart-patchwork rewrite the line-integral integrand α.toFun (γ s) (pathSpeed γ s) into a product of the continuous local coefficient and the trivialized velocity.)

theorem apply_eq_inCoordinates {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X)
    (x₀ x : X)
    (hx : x ∈ (chartAt ℂ x₀).source) (v : TangentSpace 𝓘(ℂ) x) :
    α.toFun x v =
      ContinuousLinearMap.inCoordinates ℂ (TangentSpace 𝓘(ℂ) (M := X)) ℂ (Bundle.Trivial X ℂ)
        x₀ x x₀ x (α.toFun x)
        ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x₀).continuousLinearMapAt ℂ x v)

continuousOn_form_pathSpeed

Continuous velocity tangent-section ⇒ the form integrand is ContinuousOn [0,1].

theorem continuousOn_form_pathSpeed {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (α : HolomorphicOneForms X)
    (γ : ℝ → X)
    (hvel : ContinuousOn (fun s : ℝ =>
        (Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ s) (pathSpeed γ s)))
      (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ => α.toFun (γ s) (pathSpeed γ s)) (Set.Icc 0 1)

intervalIntegrable_form_pathSpeed_of_velContinuous

Continuous velocity tangent-section ⇒ the form integrand is interval-integrable on [0,1]. The justification for the genuinely-C¹ loop predicate: the integrable field follows from the velocity-continuity (velCont) field.

theorem intervalIntegrable_form_pathSpeed_of_velContinuous {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (α : HolomorphicOneForms X) (γ : ℝ → X)
    (hvel : ContinuousOn (fun s : ℝ =>
        (Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ s) (pathSpeed γ s)))
      (Set.Icc 0 1)) :
    IntervalIntegrable (fun s : ℝ => α.toFun (γ s) (pathSpeed γ s)) MeasureTheory.volume 0 1

pathSpeed_comp_eq_mfderiv_of_mdiff

Local analogue of pathSpeed_comp_eq_mfderiv: only MDifferentiableAt f (γ t) is needed (the global ContMDiff f in the original is used solely to produce this), so it applies to local sections. The source X need *not* be compact (used with X = ℂ in the ChartBall base case).

theorem pathSpeed_comp_eq_mfderiv_of_mdiff {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    (f : X → Y) (γ : ℝ → X) (t : ℝ)
    (hf_mdiff : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f (γ t))
    (hγ_cont : ContinuousAt γ t)
    (hγ_diff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t) :
    pathSpeed (f ∘ γ) t = mfderiv 𝓘(ℂ) 𝓘(ℂ) f (γ t) (pathSpeed γ t)

velCont_comp

GLOBAL: velocity-section continuity is preserved by a global C^ω map. For the IsClosedSmoothLoop.comp constructor. Identifies velocity-section(f∘γ) with tangentMap f applied to velocity-section(γ) (pointwise via pathSpeed_comp_eq_mfderiv), then composes with the continuous tangentMap f.

theorem velCont_comp {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {Y : Type*} [TopologicalSpace Y]
    [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (γ : ℝ → X)
    (hγcont : Continuous γ)
    (hγdiff : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ s)).toFun ∘ γ) s)
    (hγ : ContinuousOn (fun s : ℝ => (Bundle.TotalSpace.mk' ℂ
      (E := TangentSpace 𝓘(ℂ) (M := X)) (γ s) (pathSpeed γ s))) (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ => (Bundle.TotalSpace.mk' ℂ
      (E := TangentSpace 𝓘(ℂ) (M := Y)) (f (γ s)) (pathSpeed (f ∘ γ) s))) (Set.Icc 0 1)

velCont_compOn

Local: velocity-section continuity is preserved by a map C^ω on an open set. For the §3 lift g∘γ (g a local section) and the ChartBall base case. Open V upgrades ContMDiffOn to ContMDiffAt/MDifferentiableAt, so pathSpeed_comp_eq_mfderiv_of_mdiff applies, and tangentMapWithin g V = tangentMap g on V. The source Y need NOT be compact (the ChartBall base case takes Y = ℂ, the non-compact model space).

theorem velCont_compOn {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y]
    (g : Y → X) {V : Set Y} (hg : ContMDiffOn 𝓘(ℂ) 𝓘(ℂ) ω g V)
    (hVo : IsOpen V) (γ : ℝ → Y) (hγV : ∀ s ∈ Set.Icc (0 : ℝ) 1, γ s ∈ V)
    (hγcont : Continuous γ)
    (hγdiff : ∀ s ∈ Set.Icc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ s)).toFun ∘ γ) s)
    (hγ : ContinuousOn (fun s : ℝ => (Bundle.TotalSpace.mk' ℂ
      (E := TangentSpace 𝓘(ℂ) (M := Y)) (γ s) (pathSpeed γ s))) (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ => (Bundle.TotalSpace.mk' ℂ
      (E := TangentSpace 𝓘(ℂ) (M := X)) (g (γ s)) (pathSpeed (g ∘ γ) s))) (Set.Icc 0 1)

velCont_reverse

Velocity-section continuity is preserved by time-reversal. For the IsClosedSmoothLoop.reverse/IsSmoothPath.reverse constructors. The reversed velocity section is s ↦ ⟨γ(1-s), -pathSpeed γ(1-s)⟩ (via pathSpeed_reverse, needs hγdiff at 1-s); base continuity comes from reparametrizing the original base by s ↦ 1-s, and the trivialized fibre is the negation of the original's (negation is ℂ-linear, passes through continuousLinearMapAt).

theorem velCont_reverse {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (γ : ℝ → X)
    (hγdiff : ∀ t ∈ Set.uIcc (0:ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t)
    (hγ : ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ s) (pathSpeed γ s))
      (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X))
          (Jacobians.reverse γ s) (pathSpeed (Jacobians.reverse γ) s))
      (Set.Icc 0 1)

pathSpeed_concat_junction

The junction velocity of a concatenation vanishes, given both pieces' chart-pullback differentiability and vanishing endpoint velocities (pathSpeed γ₁ 1 = 0, pathSpeed γ₂ 0 = 0) and matched basepoints γ₁ 1 = γ₂ 0. This is the velocity restatement of the junction step of the IsSmoothPath.concat diff field (HasDerivWithinAt … 0 glued on Iic ∪ Ici).

theorem pathSpeed_concat_junction {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (γ₁ γ₂ : ℝ → X)
    (h₁diff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ₁ 1)).toFun ∘ γ₁) 1)
    (h₂diff : DifferentiableAt ℝ ((chartAt (H := ℂ) (γ₂ 0)).toFun ∘ γ₂) 0)
    (hv₁ : pathSpeed γ₁ 1 = 0) (hv₂ : pathSpeed γ₂ 0 = 0) (hjoin : γ₁ 1 = γ₂ 0) :
    pathSpeed (Jacobians.concat γ₁ γ₂) (1/2) = 0

velCont_affineReparam

Velocity-section continuity under an affine reparametrization s ↦ a*s + b with the fibre rescaled by a. This is the shape of each half of concat (left: a = 2, b = 0; right: a = 2, b = -1), where pathSpeed (concat) s = 2 * pathSpeed γᵢ (2s + …). Mirrors velCont_reverse (itself the a = -1, b = 1 case): base continuity from reparametrizing the projection, fibre continuity from the original trivialized fibre scaled by a (scaling is ℂ-linear, passes through continuousLinearMapAt).

theorem velCont_affineReparam {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (γ : ℝ → X) (a b : ℝ) {D : Set ℝ}
    (hmaps : Set.MapsTo (fun s : ℝ => a * s + b) D (Set.Icc 0 1))
    (hγ : ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ s) (pathSpeed γ s))
      (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X))
          (γ (a * s + b)) ((a : ℂ) • pathSpeed γ (a * s + b)))
      D

velCont_reparam

Velocity-section continuity under a smooth scalar reparametrization σ. For the smoothPathSmooth = smoothPath ∘ smoothStep01 case: given the chain-rule fact pathSpeed (γ ∘ σ) s = σ'(s) • pathSpeed γ (σ s) (supplied as hspeed, from pathSpeed_smoothStep01_comp_eq), a continuous reparam σ mapping D into [0,1], and a continuous scaling σ', the reparametrized velocity section is continuous on D. Generalizes velCont_affineReparam (constant scale a) to a varying scale σ'.

theorem velCont_reparam {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (γ : ℝ → X) (σ σ' : ℝ → ℝ) {D : Set ℝ}
    (hmaps : Set.MapsTo σ D (Set.Icc 0 1)) (hσcont : ContinuousOn σ D)
    (hσ'cont : ContinuousOn (fun s : ℝ => (σ' s : ℂ)) D)
    (hspeed : ∀ s ∈ D, pathSpeed (γ ∘ σ) s = (σ' s : ℂ) • pathSpeed γ (σ s))
    (hγ : ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ s) (pathSpeed γ s))
      (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X))
          ((γ ∘ σ) s) (pathSpeed (γ ∘ σ) s))
      D

velCont_concat

Velocity-section continuity is preserved by concatenation at vanishing junction velocities. For the IsSmoothPath.concat constructor. On each open half the concatenation's velocity section is the corresponding piece's section reparametrized (2· left, 2·-1 right) with the fibre scaled by 2 (pathSpeed_concat_left/right, via velCont_affineReparam); at the junction s = ½ both the actual junction velocity (pathSpeed_concat_junction, = 0) and each scaled-reparam value (2 • pathSpeed γ₁ 1 = 0 by hv₁, resp. hv₂) vanish and the bases match (hjoin), so the concat-section coincides with each clean reparam section up to and INCLUDING ½, and the two one-sided ContinuousWithinAts glue (ContinuousWithinAt.union on Iic ½ ∪ Ici ½ = univ).

theorem velCont_concat {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (γ₁ γ₂ : ℝ → X)
    (h₁diff : ∀ t ∈ Set.uIcc (0:ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ₁ t)).toFun ∘ γ₁) t)
    (h₂diff : ∀ t ∈ Set.uIcc (0:ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ₂ t)).toFun ∘ γ₂) t)
    (hv₁ : pathSpeed γ₁ 1 = 0) (hv₂ : pathSpeed γ₂ 0 = 0) (hjoin : γ₁ 1 = γ₂ 0)
    (hγ₁ : ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ₁ s) (pathSpeed γ₁ s))
      (Set.Icc 0 1))
    (hγ₂ : ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X)) (γ₂ s) (pathSpeed γ₂ s))
      (Set.Icc 0 1)) :
    ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := X))
          (Jacobians.concat γ₁ γ₂ s) (pathSpeed (Jacobians.concat γ₁ γ₂) s))
      (Set.Icc 0 1)

velCont_modelPath

Velocity-section continuity of a C¹ path into the model space ℂ. For ℂ the chart at any point is the identity, so pathSpeed β = deriv β and the tangent bundle is trivial; the velocity section is therefore continuous as soon as β and deriv β are. This is the base-path velocity input for the ChartBallPathSmooth case of the C¹ refactor (composed with (chartAt ℂ Q₀).symm via velCont_compOn).

theorem velCont_modelPath (β : ℝ → ℂ) (hβ : Continuous β) (hβ' : Continuous (deriv β)) :
    ContinuousOn (fun s : ℝ =>
        Bundle.TotalSpace.mk' ℂ (E := TangentSpace 𝓘(ℂ) (M := ℂ)) (β s) (pathSpeed β s))
      (Set.Icc 0 1)