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

ZeroDefectImpliesCoshHypothesis

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)

 342def ZeroDefectImpliesCoshHypothesis
 343    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) : Prop :=

proof body

Definition body.

 344  UniformDefectBound H T 0 →
 345    ∀ t : ℝ, |t| ≤ T → H t = Real.cosh (Real.sqrt hyp.curvature * t)
 346

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.