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)
110def UniformDefectBound (H : ℝ → ℝ) (T ε : ℝ) : Prop :=
proof body
Definition body.
111 ∀ t u : ℝ, |t| ≤ T → |u| ≤ T → |dAlembertDefect H t u| ≤ ε
112
113/-- The standard hypothesis bundle for the stability theorem. -/
used by (4)
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.
-
H
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
H
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
dAlembertDefect
in IndisputableMonolith.Foundation.DAlembert.Stability
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use