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

AlphaCoordinateFixationCert

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)

 201structure AlphaCoordinateFixationCert where
 202  fourth_deriv_eq_alpha_sq :
 203    ∀ α : ℝ, α ≠ 0 →
 204      deriv (deriv (deriv (deriv (CostAlphaLog α)))) 0 = α ^ 2
 205  high_calibrated_iff :
 206    ∀ α : ℝ, α ≠ 0 →
 207      (IsHighCalibratedLog (CostAlphaLog α) ↔ α ^ 2 = 1)
 208  alpha_pin :
 209    ∀ α : ℝ, 1 ≤ α →
 210      IsHighCalibratedLog (CostAlphaLog α) → α = 1
 211  alpha_one_is_J :
 212    ∀ x : ℝ, 0 < x → CostAlpha 1 x = Jcost x
 213  J_unique_under_high_calibration :
 214    ∀ α : ℝ, 1 ≤ α →
 215      IsHighCalibratedLog (CostAlphaLog α) →
 216      ∀ x : ℝ, 0 < x → CostAlpha α x = Jcost x
 217

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.