Cycle Period Estimate

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def cyclePeriodEstimate (tau_rho tau_T tau_cross1 tau_cross2 : ℝ) : ℝ :=
  tau_rho + tau_T + tau_cross1 + tau_cross2

Dependency Graph

Used by

cycle_period_pos

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:231

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file

optimal_rho_increases_with_T log_linear_standardization_rate standardization_slows price_equation_rho T_dependent_selection fixed_point_instability rhoT_limit_cycle perez_phases cycle_period_pos endogenous_tipping power_law_fluctuations rhoJ_channel_imitative rhoJ_channel_differentiated lower_rho_raises_K rhoJ_channel_zero_at_min