module module

`IndisputableMonolith.Constants.AlphaExponentialForm`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.GapWeight module_import

declarations in this module (15)

theorem alphaInv_def L57
theorem alpha_seed_positive L60
theorem alphaInv_positive L66
theorem exp_factor_bounded L71
theorem alphaInv_seed_ratio L80
theorem log_alphaInv_seed_ratio L96
theorem log_alphaInv_eq L102
def alphaInv_of_gap L124
theorem alphaInv_of_gap_at_canonical L127
theorem deriv_alphaInv_of_gap L130
theorem logarithmic_derivative_constant L155
theorem alphaInv_linear_term L200
theorem alphaInv_linear_rate L207
def exponential_form_from_constant_log_derivative L242
theorem exponential_form_uniqueness_ode_principle L257