Rho J Channel Zero At Min

theorem proved Dynamics & Crises

Documentation

Lean 4 Proof

theorem rhoJ_channel_zero_at_min {ρ_min J_dot J_val ξ_J : ℝ} :
    ξ_J * (J_dot / J_val) * (ρ_min - ρ_min) = 0 := by
  simp

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:372

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 cyclePeriodEstimate cycle_period_pos endogenous_tipping power_law_fluctuations rhoJ_channel_imitative rhoJ_channel_differentiated lower_rho_raises_K