interp

formal source

 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
 132      linarith
 133    · -- s = 0: the combination is 1 · γ₁ + 0 · γ₂ = γ₁
 134      simp [← hs_zero, hp1]
 135
 136@[simp] lemma interp_apply {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ)
 137    (hs : s ∈ Icc (0:ℝ) 1) (t : ℝ) :
 138    (interp γ₁ γ₂ s hs).toFun t = (1 - s) * γ₁.toFun t + s * γ₂.toFun t := rfl
 139
 140/-- Interpolation at `s = 0` is the first path. -/
 141lemma interp_zero {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
 142    ∀ t, (interp γ₁ γ₂ 0 ⟨le_refl 0, by norm_num⟩).toFun t = γ₁.toFun t := by
 143  intro t; simp [interp_apply]