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

IRS Critical Friction Perp

noncomputable defprovedCES Potential

Documentation

Lean 4 Proof

noncomputable def irsCriticalFrictionPerp (Tstar_base γ : ℝ) : ℝ :=
  Tstar_base * γ

Dependency Graph

Used by

irs_amplifies_diversity_window

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:266

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 generalCriticalFriction irsEffectiveCurvaturePerp weightedKnockoutLoss expectedKnockoutLoss irsFirmProfit GeneralSubCritical ConcentratedRegime