Crossing Threshold Reexport

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem crossing_threshold_reexport {P_cycle : ℝ} (hP : 0 < P_cycle)
    {n : ℕ} (hn : 0 < n) :
    1 < P_cycle ^ ((1 : ℝ) / ↑n) ↔ 1 < P_cycle :=
  activation_threshold_iff_product hP hn

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:237

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file

effectiveTrainingProductivity phieff_exceeds_phi0 phieff_ge_one_condition gcFunction gc_trivial_solution adoptionR0 adoption_threshold baumolGrowthRate baumol_limit baumol_bounded_below singularityTime singularity_time_pos two_period_overinvestment saturation_escape_rate effectiveAlpha_monotone_J collapse_at_J1