pith. machine review for the scientific record. sign in
def

functionalConvexity_status

definition
show as:
view math explainer →
module
IndisputableMonolith.Action.FunctionalConvexity
domain
Action
line
313 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Action.FunctionalConvexity on GitHub at line 313.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 310
 311/-! ## Status report -/
 312
 313def functionalConvexity_status : String :=
 314  "Action.FunctionalConvexity: actionJ_convex_on_interp, geodesic_minimizes_unconditional (0 sorry, 0 axiom)"
 315
 316end Action
 317end IndisputableMonolith

papers checked against this theorem

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