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

General Critical Friction

noncomputable defprovedCES Potential

Documentation

Lean 4 Proof

noncomputable def generalCriticalFriction
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (c d_sq : ℝ) : ℝ :=
  2 * (J - 1) * c ^ 2 * d_sq / generalCurvatureK J ρ a

Dependency Graph

Used by

Tstar_increasing_in_herfindahl rho_ordering_preserved_general_weights rho_ordering_with_herfindahl

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:253

Module Section

## General-Weight and IRS Effective Curvature Definitions

In the same file

effectiveCurvature_taylor superadditivity_with_friction correlation_robustness_degrades_faster crisis_sequence_ordering sensitivity_ratio information_shadow degradation_monotone ces_prudence_with_friction adjustmentTimescale adjustmentTimescale_diverges adjustmentTimescale_monotone adjustmentTimescale_at_zero generalEffectiveCurvatureKeff irsEffectiveCurvaturePerp irsCriticalFrictionPerp weightedKnockoutLoss expectedKnockoutLoss irsFirmProfit GeneralSubCritical ConcentratedRegime