class definition def or abbrev

`AveragingDerivation`

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

formal statement (Lean)

  49class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
  50  agrees : AgreesOnExp F
  51

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

Lean names referenced from this declaration's body.

AgreesOnExp in IndisputableMonolith.Cost decl_use
SymmUnit in IndisputableMonolith.Cost decl_use
AveragingDerivation in IndisputableMonolith.Cost.FlogEL decl_use
AgreesOnExp in IndisputableMonolith.Cost.JcostCore decl_use
AveragingDerivation in IndisputableMonolith.Cost.JcostCore decl_use
SymmUnit 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