interp_apply

formal source

 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]
 144
 145/-- Interpolation at `s = 1` is the second path. -/
 146lemma interp_one {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
 147    ∀ t, (interp γ₁ γ₂ 1 ⟨by norm_num, le_refl 1⟩).toFun t = γ₂.toFun t := by
 148  intro t; simp [interp_apply]
 149
 150/-- Interpolation preserves shared endpoints. -/
 151lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
 152    (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
 153    fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by
 154  refine ⟨?_, ?_⟩
 155  · simp [interp_apply, h.1]; ring
 156  · simp [interp_apply, h.2]; ring
 157
 158/-! ## Status report -/
 159
 160/-- Status string for the path-space module. -/
 161def pathSpace_status : String :=
 162  "Action.PathSpace: AdmissiblePath, actionJ, interp, fixedEndpoints (0 sorry, 0 axiom)"
 163
 164end Action
 165end IndisputableMonolith