lemma
proved
term proof
actionJ_def
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
72@[simp] lemma actionJ_def {a b : ℝ} (γ : AdmissiblePath a b) :
73 actionJ γ = ∫ t in a..b, Jcost (γ.toFun t) := rfl
proof body
Term-mode proof.
74
75/-- The action of any admissible path is non-negative. -/
depends on (12)
Lean names referenced from this declaration's body.
-
actionJ
in IndisputableMonolith.Action.PathSpace
decl_use
-
AdmissiblePath
in IndisputableMonolith.Action.PathSpace
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
admissible
in IndisputableMonolith.Information.Thermodynamics
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use