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

EulerBudgetUpgradeTarget

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)

 722def EulerBudgetUpgradeTarget (σ₀ : ℝ) : Prop :=

proof body

Definition body.

 723  ∃ carrier : BudgetedCarrier,
 724    carrier.logDerivBound = carrierDerivBound σ₀ ∧
 725    carrier.radius = σ₀ - 1 / 2
 726
 727/-- Any successful Euler budget upgrade automatically extends the already proved
 728regular-carrier data at `σ₀`. -/

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.