def definition def or abbrev

`pathAction`

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

formal statement (Lean)

  25noncomputable def pathAction (γ : RecognitionPath) : ℝ :=

Definition body.

  26  ∫ t in (0)..γ.T, Cost.Jcost (γ.rate t)
  27
  28/-- Positive weight w[γ] = exp(-C[γ]). -/

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

born_rule_from_C in IndisputableMonolith.Measurement.BornRule decl_use
amplitude_modulus_bridge in IndisputableMonolith.Measurement.C2ABridge decl_use
measurement_bridge_C_eq_2A in IndisputableMonolith.Measurement.C2ABridge decl_use
amplitude_mod_sq_eq_weight in IndisputableMonolith.Measurement.PathAction decl_use
pathAmplitude in IndisputableMonolith.Measurement.PathAction decl_use
pathWeight in IndisputableMonolith.Measurement.PathAction decl_use

Lean names referenced from this declaration's body.