def definition def or abbrev

`actionJ`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  69noncomputable def actionJ {a b : ℝ} (γ : AdmissiblePath a b) : ℝ :=

Definition body.

  70  ∫ t in a..b, Jcost (γ.toFun t)
  71

From the project-wide theorem graph. These declarations reference this one in their body.

actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_via_convexity in IndisputableMonolith.Action.FunctionalConvexity decl_use
principle_of_least_action in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_const_one in IndisputableMonolith.Action.PathSpace decl_use
actionJ_def in IndisputableMonolith.Action.PathSpace decl_use
actionJ_nonneg in IndisputableMonolith.Action.PathSpace decl_use
pathSpace_status in IndisputableMonolith.Action.PathSpace decl_use

Lean names referenced from this declaration's body.