Documentation

Lean 4 Proof

theorem rhoJ_channel_imitative {ρ ρ_min ρ_max J_dot J_val ξ_J : ℝ}
    (hρ_range : ρ_min < ρ) (hρ_max : ρ < ρ_max)
    (hJ_pos : 0 < J_val) (hJ_growth : 0 < J_dot)
    (hξ_imitative : 0 < ξ_J) :
    -- Channel 5 contribution: ξ_J · (J_dot/J) · (ρ - ρ_min) > 0
    0 < ξ_J * (J_dot / J_val) * (ρ - ρ_min) := by
  apply mul_pos
  · apply mul_pos hξ_imitative
    exact div_pos hJ_growth hJ_pos
  · linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EndogenousRho.lean:312

Module Section

Results 70-79: Endogenous Complementarity Evolution

In the same file