actionJ_def

formal source

  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 γ₂ γ₃) :