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

interp

show as:
view Lean formalization →

The interp definition supplies the convex combination of any two admissible paths on a shared interval, weighted by s in the closed unit interval, and confirms the result remains admissible. Variational analysts working on the J-action in Recognition Science cite this to enable convexity arguments for the integrated functional. The construction substitutes the linear combination into the path structure and verifies continuity plus strict positivity via scaled sums and case analysis on the weight.

claimLet $a,b$ be reals with $a≤b$, let $γ_1,γ_2$ be admissible paths on $[a,b]$, and let $s∈[0,1]$. The interpolated path $γ$ is defined pointwise by $γ(t):=(1-s)γ_1(t)+sγ_2(t)$ for $t∈[a,b]$. Then $γ$ is continuous and strictly positive on $[a,b]$, hence admissible.

background

The PathSpace module defines admissible paths as continuous strictly positive functions on a closed interval $[a,b]$, the J-action as the integral of J-cost along such a path, and the fixed-endpoints relation. The module records that admissible paths are closed under convex combinations; this fact is stated explicitly to support the convexity proofs that follow in FunctionalConvexity. Upstream, the admissible-path structure supplies the continuity and positivity fields that any interpolation must preserve, as quoted in the module documentation: admissible paths are continuous, strictly positive functions.

proof idea

The definition installs the pointwise linear combination as the underlying function. Continuity of the result is obtained by scaling each input path by a constant (via const_smul) and adding the results. Positivity proceeds by case distinction on whether the weight is zero or positive, applying multiplication rules for positive and nonnegative reals together with linear arithmetic to conclude strict inequality.

why it matters in Recognition Science

This definition is invoked directly by actionJ_convex_on_interp, actionJ_local_min_is_global, geodesic_minimizes_unconditional, and principle_of_least_action in FunctionalConvexity. It supplies the interpolation segment that converts pointwise convexity of J-cost into convexity of the integrated action, discharging the witness required by the unconditional least-action statements. In the Recognition framework it closes the structural requirement that lets the variational stage inherit convexity from the core J functional equation without extra positivity hypotheses.

scope and limits

Lean usage

have γ := interp γ1 γ2 s hs

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.