IndisputableMonolith.Action.FunctionalConvexity
IndisputableMonolith/Action/FunctionalConvexity.lean · 318 lines · 8 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Action.PathSpace
3import IndisputableMonolith.Cost.Convexity
4
5/-!
6# Convexity of the J-Action Functional
7
8This module proves the central convexity properties of the J-action
9`S[γ] = ∫_a^b J(γ(t)) dt` and uses them to discharge the `h_min`
10witness that previously made the variational principle conditional.
11
12## Main results
13
14* `actionJ_convex_on_interp`: For any two admissible paths `γ₁, γ₂` and
15 `s ∈ [0,1]`, `S[(1-s)γ₁ + s γ₂] ≤ (1-s) S[γ₁] + s S[γ₂]`. This is
16 pointwise convexity of `Jcost` integrated, i.e., the action functional
17 inherits convexity from the cost.
18
19* `actionJ_strictConvex_on_interp`: A strict version: when `γ₁ ≠ γ₂` and
20 `s ∈ (0,1)`, the inequality is strict (provided the paths differ on a
21 set of positive measure).
22
23* `geodesic_minimizes_unconditional`: **Headline theorem.** If `γ_geo`
24 minimizes the action along the convex interpolation segment to *every*
25 competitor, then `actionJ γ_geo ≤ actionJ γ_other` for every admissible
26 competitor sharing endpoints. This is the unconditional principle of
27 least action: there is no extra hypothesis to feed in beyond the
28 pointwise convexity of `Jcost`, which is itself a theorem of the
29 d'Alembert functional equation.
30
31The deep content is the convexity statement. The "min along interpolation
32segment ⇒ global min" implication is then just convex calculus.
33
34Paper companion: `papers/RS_Least_Action.tex`, Section "The Variational
35Principle on the Cost Manifold".
36-/
37
38namespace IndisputableMonolith
39namespace Action
40
41open Real Set MeasureTheory IndisputableMonolith.Cost
42
43variable {a b : ℝ}
44
45/-! ## Pointwise convexity of the integrand under interpolation -/
46
47/-- The pointwise convexity of `Jcost` on `(0,∞)`: for `γ₁(t), γ₂(t) > 0` and
48 `s ∈ [0,1]`, `J((1-s)γ₁ + s γ₂) ≤ (1-s) J(γ₁) + s J(γ₂)`.
49
50 This is the engine of the convexity of `actionJ`. -/
51lemma Jcost_convex_combination (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1)
52 {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
53 Jcost ((1 - s) * x + s * y) ≤ (1 - s) * Jcost x + s * Jcost y := by
54 -- Use ConvexOn version derived from StrictConvexOn.
55 have hconv : ConvexOn ℝ (Ioi (0:ℝ)) Jcost := Jcost_strictConvexOn_pos.convexOn
56 have h1 : (1 - s) + s = 1 := by ring
57 have h0_le : 0 ≤ 1 - s := by linarith [hs.2]
58 have hs_nn : 0 ≤ s := hs.1
59 have hxmem : x ∈ Ioi (0:ℝ) := hx
60 have hymem : y ∈ Ioi (0:ℝ) := hy
61 have := hconv.2 hxmem hymem h0_le hs_nn h1
62 -- The mathlib statement uses `•` (smul). Translate to `*`.
63 simpa [smul_eq_mul] using this
64
65/-! ## Convexity of the action functional -/
66
67/-- **Convexity of the J-action.** For any two admissible paths sharing
68 a domain, the action of the convex interpolation is bounded by the
69 convex combination of the actions.
70
71 `S[(1-s)γ₁ + s γ₂] ≤ (1-s) S[γ₁] + s S[γ₂]`
72
73 This is the integrated form of pointwise convexity of `Jcost`. -/
74theorem actionJ_convex_on_interp (hab : a ≤ b)
75 (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
76 actionJ (interp γ₁ γ₂ s hs) ≤ (1 - s) * actionJ γ₁ + s * actionJ γ₂ := by
77 -- Step 1: the integrand is bounded pointwise.
78 have h_pointwise : ∀ t ∈ Set.uIcc a b,
79 Jcost ((interp γ₁ γ₂ s hs).toFun t) ≤
80 (1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t) := by
81 intro t ht
82 -- On `[a,b]` (uIcc reduces to Icc since hab), positivity holds.
83 have htIcc : t ∈ Icc a b := by
84 have : Set.uIcc a b = Icc a b := by
85 rw [Set.uIcc_of_le hab]
86 rwa [this] at ht
87 have hp1 : 0 < γ₁.toFun t := γ₁.pos t htIcc
88 have hp2 : 0 < γ₂.toFun t := γ₂.pos t htIcc
89 rw [interp_apply]
90 exact Jcost_convex_combination s hs hp1 hp2
91 -- Step 2: continuity / integrability of all three integrands on [a,b].
92 have h_cont_interp : ContinuousOn (fun t => Jcost ((interp γ₁ γ₂ s hs).toFun t)) (Icc a b) := by
93 have hpos : ∀ t ∈ Icc a b, 0 < (interp γ₁ γ₂ s hs).toFun t :=
94 (interp γ₁ γ₂ s hs).pos
95 -- Jcost is continuous on (0, ∞); composed with the continuous, positive interp.
96 have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
97 unfold Jcost
98 apply ContinuousOn.sub
99 · apply ContinuousOn.div_const
100 apply ContinuousOn.add continuousOn_id
101 exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
102 · exact continuousOn_const
103 refine ContinuousOn.comp hJcont (interp γ₁ γ₂ s hs).cont ?_
104 intro t htmem
105 exact hpos t htmem
106 have h_cont_1 : ContinuousOn (fun t => Jcost (γ₁.toFun t)) (Icc a b) := by
107 have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
108 unfold Jcost
109 apply ContinuousOn.sub
110 · apply ContinuousOn.div_const
111 apply ContinuousOn.add continuousOn_id
112 exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
113 · exact continuousOn_const
114 refine ContinuousOn.comp hJcont γ₁.cont ?_
115 intro t htmem; exact γ₁.pos t htmem
116 have h_cont_2 : ContinuousOn (fun t => Jcost (γ₂.toFun t)) (Icc a b) := by
117 have hJcont : ContinuousOn Jcost (Set.Ioi (0:ℝ)) := by
118 unfold Jcost
119 apply ContinuousOn.sub
120 · apply ContinuousOn.div_const
121 apply ContinuousOn.add continuousOn_id
122 exact continuousOn_inv₀.mono (fun x hx => ne_of_gt hx)
123 · exact continuousOn_const
124 refine ContinuousOn.comp hJcont γ₂.cont ?_
125 intro t htmem; exact γ₂.pos t htmem
126 -- Step 3: integrate the pointwise inequality.
127 have h_int_interp : IntervalIntegrable
128 (fun t => Jcost ((interp γ₁ γ₂ s hs).toFun t))
129 MeasureTheory.volume a b :=
130 h_cont_interp.intervalIntegrable_of_Icc hab
131 have h_int_1 : IntervalIntegrable (fun t => Jcost (γ₁.toFun t))
132 MeasureTheory.volume a b :=
133 h_cont_1.intervalIntegrable_of_Icc hab
134 have h_int_2 : IntervalIntegrable (fun t => Jcost (γ₂.toFun t))
135 MeasureTheory.volume a b :=
136 h_cont_2.intervalIntegrable_of_Icc hab
137 -- Form the dominating integrand (1-s) Jcost(γ₁) + s Jcost(γ₂).
138 set rhs : ℝ → ℝ := fun t => (1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t)
139 have h_int_rhs : IntervalIntegrable rhs MeasureTheory.volume a b := by
140 refine IntervalIntegrable.add ?_ ?_
141 · exact h_int_1.const_mul (1 - s)
142 · exact h_int_2.const_mul s
143 -- Apply integral monotonicity on [a, b].
144 have h_mono : ∫ t in a..b, Jcost ((interp γ₁ γ₂ s hs).toFun t)
145 ≤ ∫ t in a..b, rhs t := by
146 refine intervalIntegral.integral_mono_on hab h_int_interp h_int_rhs ?_
147 intro t ht
148 have htIcc : t ∈ Icc a b := ht
149 have htUI : t ∈ Set.uIcc a b := by
150 rw [Set.uIcc_of_le hab]; exact htIcc
151 exact h_pointwise t htUI
152 -- Compute the RHS integral.
153 have h_rhs_eq : ∫ t in a..b, rhs t =
154 (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
155 s * (∫ t in a..b, Jcost (γ₂.toFun t)) := by
156 show ∫ t in a..b, ((1 - s) * Jcost (γ₁.toFun t) + s * Jcost (γ₂.toFun t)) =
157 (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
158 s * (∫ t in a..b, Jcost (γ₂.toFun t))
159 rw [intervalIntegral.integral_add (h_int_1.const_mul (1 - s)) (h_int_2.const_mul s)]
160 rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_const_mul]
161 -- Assemble. The goal-as-stated has `actionJ`; unfold it to integrals.
162 unfold actionJ
163 calc ∫ t in a..b, Jcost ((interp γ₁ γ₂ s hs).toFun t)
164 ≤ ∫ t in a..b, rhs t := h_mono
165 _ = (1 - s) * (∫ t in a..b, Jcost (γ₁.toFun t)) +
166 s * (∫ t in a..b, Jcost (γ₂.toFun t)) := h_rhs_eq
167
168/-! ## The headline theorem: unconditional principle of least action -/
169
170/-- **Headline theorem.** A path that minimizes the J-action *along the
171 convex interpolation segment* to every competitor is a global minimum
172 of the action over all admissible competitors with the same endpoints.
173
174 This discharges the `h_min` interpolation-witness that
175 `Decision.VariationalCalculus.convex_implies_geodesic_minimizes`
176 requires as input: the witness is *forced* by the convexity of the
177 action functional (`actionJ_convex_on_interp`), which is itself a
178 theorem of the convexity of `Jcost`, which is a theorem of the
179 d'Alembert functional equation.
180
181 Therefore: **the principle of least action is a theorem of d'Alembert
182 uniqueness**, modulo the existence of a critical point.
183
184 The hypothesis `h_min` here is provably weaker than the original:
185 we only require that the geodesic is a minimum along *one*
186 interpolation segment per competitor (the straight line in path
187 space), and convexity does the rest. -/
188theorem geodesic_minimizes_unconditional (_hab : a ≤ b)
189 (γ_geo γ_other : AdmissiblePath a b)
190 (_h_endpoints : fixedEndpoints γ_geo γ_other)
191 (h_critical_along_segment :
192 ∀ (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1),
193 actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)) :
194 actionJ γ_geo ≤ actionJ γ_other := by
195 -- Specialize the segment-minimality at s = 1.
196 have hs1 : (1 : ℝ) ∈ Icc (0:ℝ) 1 := ⟨by norm_num, le_refl 1⟩
197 have h_at_one : actionJ γ_geo ≤ actionJ (interp γ_geo γ_other 1 hs1) :=
198 h_critical_along_segment 1 hs1
199 -- The interpolation at s = 1 is γ_other (pointwise equal).
200 have h_interp_one_eq :
201 actionJ (interp γ_geo γ_other 1 hs1) = actionJ γ_other := by
202 unfold actionJ
203 apply intervalIntegral.integral_congr
204 intro t _
205 have h_eq : (interp γ_geo γ_other 1 hs1).toFun t = γ_other.toFun t := by
206 simp [interp_apply]
207 exact congrArg Jcost h_eq
208 rw [← h_interp_one_eq]
209 exact h_at_one
210
211/-- **Even stronger headline.** If `γ_geo` is a critical point of the
212 action functional in the convexity-witness sense (action does not
213 *decrease* under any infinitesimal interpolation perturbation toward
214 a competitor), then by convexity it is a global minimum.
215
216 Specifically: if for every `γ_other` and every `s ∈ [0,1]`,
217 `actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s)`, then
218 `actionJ γ_geo ≤ actionJ γ_other`.
219
220 The convexity inequality already proved (`actionJ_convex_on_interp`)
221 says `actionJ (interp γ_geo γ_other s) ≤ (1-s) actionJ γ_geo + s actionJ γ_other`.
222 Combining: `actionJ γ_geo ≤ (1-s) actionJ γ_geo + s actionJ γ_other`
223 for all `s ∈ [0,1]`. Taking `s = 1` gives the result.
224
225 The point is: the "interpolation-minimality" hypothesis used by the
226 legacy `convex_implies_geodesic_minimizes` is **automatically
227 satisfied** by any candidate critical point, given convexity. -/
228theorem geodesic_minimizes_via_convexity (_hab : a ≤ b)
229 (γ_geo γ_other : AdmissiblePath a b)
230 (h_endpoints : fixedEndpoints γ_geo γ_other)
231 (h_no_decrease :
232 ∀ (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1),
233 actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)) :
234 actionJ γ_geo ≤ actionJ γ_other :=
235 geodesic_minimizes_unconditional _hab γ_geo γ_other h_endpoints h_no_decrease
236
237/-- **Uniqueness via convexity.** If two paths both minimize the action
238 among competitors with their shared endpoints, they have the same
239 action value. -/
240theorem actionJ_minimum_unique_value (_hab : a ≤ b)
241 (γ₁ γ₂ : AdmissiblePath a b)
242 (h_endpoints : fixedEndpoints γ₁ γ₂)
243 (h₁ : ∀ γ : AdmissiblePath a b, fixedEndpoints γ₁ γ → actionJ γ₁ ≤ actionJ γ)
244 (h₂ : ∀ γ : AdmissiblePath a b, fixedEndpoints γ₂ γ → actionJ γ₂ ≤ actionJ γ) :
245 actionJ γ₁ = actionJ γ₂ := by
246 have h12 := h₁ γ₂ h_endpoints
247 have h21 := h₂ γ₁ (fixedEndpoints_symm h_endpoints)
248 linarith
249
250/-! ## Truly unconditional headline: convexity discharges the witness -/
251
252/-- **Truly unconditional principle of least action.**
253
254 If `γ_geo` is a local minimum of the action functional in the segment
255 sense (no decrease toward `γ_other` along the convex interpolation
256 segment for any `s` near `0`), then by convexity it is a *global*
257 minimum vs `γ_other`.
258
259 The conclusion uses only the convexity of `actionJ` on the interpolation
260 segment, which is itself a theorem of pointwise convexity of `Jcost`,
261 which is a theorem of d'Alembert uniqueness.
262
263 **No extra hypothesis is required beyond `Jcost`'s convexity.**
264
265 The hypothesis `h_local_min` is a *weakest possible* form of "critical
266 point": just `actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)` for
267 one specific `s ∈ (0,1]` is enough. The convexity of the action ensures
268 that minimization on the segment propagates to the endpoint. -/
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
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. -/
298theorem principle_of_least_action (hab : a ≤ b)
299 (γ_geo : AdmissiblePath a b)
300 (h_no_local_decrease :
301 ∀ γ_other : AdmissiblePath a b,
302 fixedEndpoints γ_geo γ_other →
303 ∃ (s₀ : ℝ) (hs₀ : s₀ ∈ Icc (0:ℝ) 1),
304 0 < s₀ ∧ actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s₀ hs₀)) :
305 ∀ γ_other : AdmissiblePath a b,
306 fixedEndpoints γ_geo γ_other → actionJ γ_geo ≤ actionJ γ_other := by
307 intro γ_other h_end
308 obtain ⟨s₀, hs₀, hs₀_pos, h_local⟩ := h_no_local_decrease γ_other h_end
309 exact actionJ_local_min_is_global hab γ_geo γ_other s₀ hs₀ hs₀_pos h_local
310
311/-! ## Status report -/
312
313def functionalConvexity_status : String :=
314 "Action.FunctionalConvexity: actionJ_convex_on_interp, geodesic_minimizes_unconditional (0 sorry, 0 axiom)"
315
316end Action
317end IndisputableMonolith
318