def definition def or abbrev

`AgreesOnExp`

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

formal statement (Lean)

  34def AgreesOnExp (F : ℝ → ℝ) : Prop := ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)

proof body

Definition body.

used by (12)

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

agree_on_exp_extends in IndisputableMonolith.Cost decl_use
agrees_on_exp_of_bounds in IndisputableMonolith.Cost decl_use
agrees_on_exp_of_symm_unit in IndisputableMonolith.Cost decl_use
AveragingAgree in IndisputableMonolith.Cost decl_use
AveragingDerivation in IndisputableMonolith.Cost decl_use
F_eq_J_on_pos in IndisputableMonolith.Cost decl_use
F_eq_J_on_pos_alt in IndisputableMonolith.Cost decl_use
T5_cost_uniqueness_on_pos in IndisputableMonolith.Cost decl_use
AgreesOnExp in IndisputableMonolith.Cost.JcostCore decl_use
AveragingAgree in IndisputableMonolith.Cost.JcostCore decl_use
AveragingDerivation in IndisputableMonolith.Cost.JcostCore decl_use
Jcost_agrees_on_exp in IndisputableMonolith.Cost.JcostCore decl_use

depends on (4)

Lean names referenced from this declaration's body.

AgreesOnExp in IndisputableMonolith.Cost.JcostCore decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use