module module

`IndisputableMonolith.Action.FunctionalConvexity`

show as: view Lean formalization →

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

generate prose now

used by (2)

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

IndisputableMonolith.Action.EulerLagrange module_import
IndisputableMonolith.Action.QuadraticLimit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Action.PathSpace module_import
IndisputableMonolith.Cost.Convexity module_import

declarations in this module (8)

lemma Jcost_convex_combination L51
theorem actionJ_convex_on_interp L74
theorem geodesic_minimizes_unconditional L188
theorem geodesic_minimizes_via_convexity L228
theorem actionJ_minimum_unique_value L240
theorem actionJ_local_min_is_global L269
theorem principle_of_least_action L298
def functionalConvexity_status L313