pith. machine review for the scientific record. sign in
def definition def or abbrev

interp

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Definition body.

 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

used by (14)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.