Sections / Section 9: CES Potential and Information Friction / curvatureK_abs_substitute

Curvature K Abs Substitute

theoremprovedDynamics & Crises

Documentation

Lean 4 Proof

theorem curvatureK_abs_substitute (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 1 < ρ) :
    |curvatureK J ρ| = (ρ - 1) * (↑J - 1) / ↑J := by
  rw [abs_of_neg (curvatureK_neg_substitute hJ hρ)]
  simp only [curvatureK]; ring

Dependency Graph

Location

thesis/CESProofs/Potential/SubstituteRegime.lean:50

Module Section

Substitute Regime: The ρ > 1 Theory (Anti-Complementarity)

In the same file

curvatureK_neg_substitute eigenvalue_perp_pos_substitute cesHessianQF_pos_semidef_substitute cesHessianQF_pos_on_perp subadditivity_qualitative hessianQF_eq_negK_norm strategic_instability specializationRatio specialization_dominates diversification_dominates boundary_indifference regime_trichotomy manipulation_magnitude escort_amplifies_leader escort_compresses_leader superadditivity_reverses_substitutes correlation_amplification_substitutes