module
module
IndisputableMonolith.Foundation.AlphaCoordinateFixation
show as:
view Lean formalization →
used by (1)
depends on (2)
declarations in this module (16)
-
lemma
hasDerivAt_costAlphaLog_first -
lemma
deriv_costAlphaLog_eq -
lemma
hasDerivAt_costAlphaLog_second -
lemma
deriv_deriv_costAlphaLog_eq -
lemma
hasDerivAt_costAlphaLog_third -
lemma
deriv_deriv_deriv_costAlphaLog_eq -
lemma
hasDerivAt_costAlphaLog_fourth -
theorem
costAlphaLog_fourth_deriv_at_zero -
def
IsHighCalibratedLog -
theorem
costAlphaLog_high_calibrated_iff -
theorem
alpha_pin_under_high_calibration -
theorem
alpha_pinned_to_one_implies_J -
theorem
J_uniquely_calibrated_via_higher_derivative -
structure
AlphaCoordinateFixationCert -
def
alphaCoordinateFixationCert -
theorem
alphaCoordinateFixationCert_inhabited