  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.