pith. machine review for the scientific record. sign in
def definition def or abbrev

ClassifiedLogCost

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)

 329def ClassifiedLogCost (G : ℝ → ℝ) : Prop :=

proof body

Definition body.

 330  (∀ t, G t = 0) ∨
 331  (∃ α : ℝ, ∀ t, G t = α * t^2) ∨
 332  (∃ α : ℝ, ∀ t, G t = Real.cosh (α * t) - 1) ∨
 333  (∃ α : ℝ, ∀ t, G t = 1 - Real.cos (α * t))
 334
 335/-- The zero log-cost satisfies the bilinear identity with any coefficient. -/

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.