IndisputableMonolith.Action.PathSpace

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.Convexity
   4
   5/-!
   6# Path Space and the J-Action Functional
   7
   8This module sets up the variational stage for the principle of least action
   9derived from the d'Alembert cost functional `J`. It defines:
  10
  11* `AdmissiblePath a b`: continuous, strictly positive paths on `[a, b]`,
  12* `actionJ γ`: the J-action `∫ J(γ(t)) dt`,
  13* `fixedEndpoints γ₁ γ₂`: the boundary-condition relation,
  14* `interp γ₁ γ₂ s`: the straight-line interpolation in path space.
  15
  16Paper companion: `papers/RS_Least_Action.tex`.
  17
  18The crucial structural fact, recorded here, is that admissible paths are
  19closed under convex interpolation: if `γ₁` and `γ₂` are positive on `[a,b]`,
  20so is any `(1-s) γ₁ + s γ₂` with `s ∈ [0,1]`. This is what enables the
  21strict-convexity argument of `Action.FunctionalConvexity` to work without
  22any extra positivity hypothesis.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Action
  27
  28open Real Set MeasureTheory IndisputableMonolith.Cost
  29
  30/-! ## Admissible paths -/
  31
  32/-- An admissible path on `[a, b]` is a continuous, strictly positive function. -/
  33structure AdmissiblePath (a b : ℝ) where
  34  /-- The underlying function. -/
  35  toFun : ℝ → ℝ
  36  /-- Continuity on the closed interval. -/
  37  cont : ContinuousOn toFun (Icc a b)
  38  /-- Strict positivity on the closed interval. -/
  39  pos : ∀ t ∈ Icc a b, 0 < toFun t
  40
  41namespace AdmissiblePath
  42
  43variable {a b : ℝ}
  44
  45instance : CoeFun (AdmissiblePath a b) (fun _ => ℝ → ℝ) := ⟨AdmissiblePath.toFun⟩
  46
  47@[simp] lemma coe_mk (f : ℝ → ℝ) (hc : ContinuousOn f (Icc a b))
  48    (hp : ∀ t ∈ Icc a b, 0 < f t) :
  49    (⟨f, hc, hp⟩ : AdmissiblePath a b).toFun = f := rfl
  50
  51/-- The constant path at value `c > 0`. -/
  52def const (a b c : ℝ) (hc : 0 < c) : AdmissiblePath a b where
  53  toFun := fun _ => c
  54  cont := continuousOn_const
  55  pos := fun _ _ => hc
  56
  57@[simp] lemma const_apply {a b c : ℝ} (hc : 0 < c) (t : ℝ) :
  58    (const a b c hc).toFun t = c := rfl
  59
  60end AdmissiblePath
  61
  62/-! ## The J-action functional -/
  63
  64/-- The J-action functional `S[γ] = ∫_a^b J(γ(t)) dt`.
  65
  66    This is the central object of the variational principle. Geodesics of
  67    the Hessian metric `g(x) = J''(x) = 1/x³` minimize this functional
  68    among admissible paths with fixed endpoints. -/
  69noncomputable def actionJ {a b : ℝ} (γ : AdmissiblePath a b) : ℝ :=
  70  ∫ t in a..b, Jcost (γ.toFun t)
  71
  72@[simp] lemma actionJ_def {a b : ℝ} (γ : AdmissiblePath a b) :
  73    actionJ γ = ∫ t in a..b, Jcost (γ.toFun t) := rfl
  74
  75/-- The action of any admissible path is non-negative. -/
  76lemma actionJ_nonneg {a b : ℝ} (hab : a ≤ b) (γ : AdmissiblePath a b) :
  77    0 ≤ actionJ γ := by
  78  unfold actionJ
  79  exact intervalIntegral.integral_nonneg hab
  80    (fun t ht => Jcost_nonneg (γ.pos t ht))
  81
  82/-- The action of the constant path at `1` (the cost-minimum) vanishes. -/
  83lemma actionJ_const_one {a b : ℝ} :
  84    actionJ (AdmissiblePath.const a b 1 one_pos) = 0 := by
  85  unfold actionJ
  86  simp [AdmissiblePath.const_apply, Jcost_unit0]
  87
  88/-! ## Fixed endpoints -/
  89
  90/-- Two admissible paths share endpoints. -/
  91def fixedEndpoints {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) : Prop :=
  92  γ₁.toFun a = γ₂.toFun a ∧ γ₁.toFun b = γ₂.toFun b
  93
  94lemma fixedEndpoints_refl {a b : ℝ} (γ : AdmissiblePath a b) :
  95    fixedEndpoints γ γ := And.intro rfl rfl
  96
  97lemma fixedEndpoints_symm {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
  98    (h : fixedEndpoints γ₁ γ₂) : fixedEndpoints γ₂ γ₁ :=
  99  ⟨h.1.symm, h.2.symm⟩
 100
 101lemma fixedEndpoints_trans {a b : ℝ} {γ₁ γ₂ γ₃ : AdmissiblePath a b}
 102    (h₁ : fixedEndpoints γ₁ γ₂) (h₂ : fixedEndpoints γ₂ γ₃) :
 103    fixedEndpoints γ₁ γ₃ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩
 104
 105/-! ## Convex interpolation in path space -/
 106
 107/-- The straight-line interpolation between two admissible paths.
 108
 109    `interp γ₁ γ₂ s = (1 - s) · γ₁ + s · γ₂`.
 110
 111    The key structural fact is that for `s ∈ [0,1]`, this convex combination
 112    is again strictly positive and continuous, hence again admissible. -/
 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
 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
 136@[simp] lemma interp_apply {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) (s : ℝ)
 137    (hs : s ∈ Icc (0:ℝ) 1) (t : ℝ) :
 138    (interp γ₁ γ₂ s hs).toFun t = (1 - s) * γ₁.toFun t + s * γ₂.toFun t := rfl
 139
 140/-- Interpolation at `s = 0` is the first path. -/
 141lemma interp_zero {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
 142    ∀ t, (interp γ₁ γ₂ 0 ⟨le_refl 0, by norm_num⟩).toFun t = γ₁.toFun t := by
 143  intro t; simp [interp_apply]
 144
 145/-- Interpolation at `s = 1` is the second path. -/
 146lemma interp_one {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
 147    ∀ t, (interp γ₁ γ₂ 1 ⟨by norm_num, le_refl 1⟩).toFun t = γ₂.toFun t := by
 148  intro t; simp [interp_apply]
 149
 150/-- Interpolation preserves shared endpoints. -/
 151lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
 152    (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
 153    fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by
 154  refine ⟨?_, ?_⟩
 155  · simp [interp_apply, h.1]; ring
 156  · simp [interp_apply, h.2]; ring
 157
 158/-! ## Status report -/
 159
 160/-- Status string for the path-space module. -/
 161def pathSpace_status : String :=
 162  "Action.PathSpace: AdmissiblePath, actionJ, interp, fixedEndpoints (0 sorry, 0 axiom)"
 163
 164end Action
 165end IndisputableMonolith
 166