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

Critical Friction

defprovedCES Potential

Documentation

Lean 4 Proof

def criticalFriction (J : ℕ) (ρ c d_sq : ℝ) : ℝ :=
  2 * (↑J - 1) * c ^ 2 * d_sq / curvatureK J ρ

Dependency Graph

Used by

sectoral_recession_ordering recovery_ordering rho_ordering_criticalFriction rho_drift_shifts_Tstar sectorCriticalFriction relaxation_rate_vanishes_at_Tstar complementary_sectors_smaller_margin sectorCriticalFriction_pos complementary_goods_more_fragile efficiency_fragility_tradeoff

Location

thesis/CESProofs/Potential/Defs.lean:137

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file

qLog qExp qLog_one qExp_zero qLog_eq_of_ne qExp_eq_of_ne OnSimplex OnOpenSimplex tsallisEntropy tsallisEntropy_uniform cesPotential effectiveCurvatureKeff effectiveCurvatureKeff_zero_friction effectiveCurvatureKeff_above_critical effectiveCurvatureKeff_nonneg effectiveCurvatureKeff_le_K effectiveCurvatureKeff_pos uniform_onOpenSimplex OnOpenSimplex.toSimplex cesPotential_uniform_equal