fixedEndpoints_trans

formal source

  98    (h : fixedEndpoints γ₁ γ₂) : fixedEndpoints γ₂ γ₁ :=
  99  ⟨h.1.symm, h.2.symm⟩
 100
 101lemma fixedEndpoints_trans {a b : ℝ} {γ₁ γ₂ γ₃ : AdmissiblePath a b}
 102    (h₁ : fixedEndpoints γ₁ γ₂) (h₂ : fixedEndpoints γ₂ γ₃) :
 103    fixedEndpoints γ₁ γ₃ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩
 104
 105/-! ## Convex interpolation in path space -/
 106
 107/-- The straight-line interpolation between two admissible paths.
 108
 109    `interp γ₁ γ₂ s = (1 - s) · γ₁ + s · γ₂`.
 110
 111    The key structural fact is that for `s ∈ [0,1]`, this convex combination
 112    is again strictly positive and continuous, hence again admissible. -/
 113def interp {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ)
 114    (hs : s ∈ Icc (0:ℝ) 1) : AdmissiblePath a b where
 115  toFun := fun t => (1 - s) * γ₁.toFun t + s * γ₂.toFun t
 116  cont := by
 117    have h1 : ContinuousOn (fun t => (1 - s) * γ₁.toFun t) (Icc a b) :=
 118      γ₁.cont.const_smul (1 - s) |>.congr (fun _ _ => by simp [smul_eq_mul])
 119    have h2 : ContinuousOn (fun t => s * γ₂.toFun t) (Icc a b) :=
 120      γ₂.cont.const_smul s |>.congr (fun _ _ => by simp [smul_eq_mul])
 121    exact h1.add h2
 122  pos := by
 123    intro t ht
 124    have h1s : 0 ≤ 1 - s := by linarith [hs.2]
 125    have hs' : 0 ≤ s := hs.1
 126    have hp1 : 0 < γ₁.toFun t := γ₁.pos t ht
 127    have hp2 : 0 < γ₂.toFun t := γ₂.pos t ht
 128    -- Either s = 0 (LHS pure γ₁), or s > 0 (RHS strictly positive). Either way > 0.
 129    rcases lt_or_eq_of_le hs' with hs_pos | hs_zero
 130    · have := mul_pos hs_pos hp2
 131      have hnn : 0 ≤ (1 - s) * γ₁.toFun t := mul_nonneg h1s hp1.le