const

formal source

  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. -/