Documentation

Lean 4 Proof

theorem saturation_escape_rate {Delta_Phi T tau_0 : ℝ}
    (_hDelta : 0 < Delta_Phi) (_hT : 0 < T) (htau : 0 < tau_0) :
    0 < tau_0 * Real.exp (Delta_Phi / T) :=
  mul_pos htau (Real.exp_pos _)

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:194

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file