theorem
proved
tactic proof
actionJ_local_min_is_global
show as:
view Lean formalization →
formal statement (Lean)
269theorem actionJ_local_min_is_global (hab : a ≤ b)
270 (γ_geo γ_other : AdmissiblePath a b)
271 (s₀ : ℝ) (hs₀ : s₀ ∈ Icc (0:ℝ) 1) (hs₀_pos : 0 < s₀)
272 (h_local_min : actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s₀ hs₀)) :
273 actionJ γ_geo ≤ actionJ γ_other := by
proof body
Tactic-mode proof.
274 -- By convexity of actionJ on the segment:
275 -- actionJ (interp γ_geo γ_other s₀ hs₀) ≤ (1-s₀) actionJ γ_geo + s₀ actionJ γ_other
276 have h_conv := actionJ_convex_on_interp hab γ_geo γ_other s₀ hs₀
277 -- Combine with local minimality:
278 -- actionJ γ_geo ≤ (1-s₀) actionJ γ_geo + s₀ actionJ γ_other
279 have h_combine : actionJ γ_geo ≤ (1 - s₀) * actionJ γ_geo + s₀ * actionJ γ_other :=
280 le_trans h_local_min h_conv
281 -- Rearrange: s₀ · actionJ γ_geo ≤ s₀ · actionJ γ_other
282 -- actionJ γ_geo - (1 - s₀) actionJ γ_geo ≤ s₀ * actionJ γ_other
283 -- s₀ · actionJ γ_geo ≤ s₀ · actionJ γ_other
284 -- Since s₀ > 0, divide: actionJ γ_geo ≤ actionJ γ_other.
285 have h_factor : s₀ * actionJ γ_geo ≤ s₀ * actionJ γ_other := by linarith
286 exact le_of_mul_le_mul_left h_factor hs₀_pos
287
288/-- **The principle of least action, unconditionally.**
289
290 If `γ_geo` does not decrease the action on the way to *any* competitor
291 `γ_other` (along the straight-line interpolation in path space, at
292 even one positive step), then `γ_geo` minimizes the action globally
293 among all admissible competitors with the same endpoints.
294
295 This is the clean unconditional version, with no extra
296 interpolation-minimality witness. The witness is *replaced* by
297 convexity, which is *proved* from the d'Alembert functional equation. -/