interp_apply
plain-language theorem explainer
The interp_apply lemma states that the pointwise value of the interpolated path between two admissible paths γ₁ and γ₂ at parameter s equals the convex combination (1-s)γ₁(t) + sγ₂(t). Variational analysts working on the J-action would cite this when verifying that interpolation commutes with evaluation in the path space. The proof is a one-line reflexivity that unfolds the definition of interp.
Claim. Let γ₁, γ₂ be continuous strictly positive functions on [a, b]. For s ∈ [0, 1] and any real t, the interpolated path satisfies [(1-s)γ₁ + sγ₂](t) = (1-s)γ₁(t) + sγ₂(t).
background
In the PathSpace module the admissible path structure requires a continuous function on the closed interval [a, b] that is strictly positive everywhere on that interval. The interp definition constructs the straight-line interpolation as the pointwise convex combination (1-s)γ₁ + sγ₂ and proves that this combination remains continuous and strictly positive, hence admissible, for every s in [0, 1]. This closure property is the key structural fact recorded in the module that lets the subsequent convexity argument proceed without extra positivity hypotheses.
proof idea
The proof is a one-line term-mode reflexivity that directly matches the toFun field of the interp construction to the explicit linear combination (1-s)·γ₁.toFun + s·γ₂.toFun.
why it matters
This lemma is invoked by actionJ_convex_on_interp to obtain the pointwise inequality needed for the integrated convexity of the J-action, and by geodesic_minimizes_unconditional to discharge the interpolation-witness hypothesis in the global minimization statement. It therefore sits at the base of the variational stage for the principle of least action derived from the d'Alembert cost functional J, as described in the module companion paper RS_Least_Action.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.