fixedEndpoints_symm

formal source

  94lemma fixedEndpoints_refl {a b : ℝ} (γ : AdmissiblePath a b) :
  95    fixedEndpoints γ γ := And.intro rfl rfl
  96
  97lemma fixedEndpoints_symm {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
  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