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

General Effective Curvature Keff

noncomputable defprovedCES Potential

Documentation

Lean 4 Proof

noncomputable def generalEffectiveCurvatureKeff
    (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) (T Tstar : ℝ) : ℝ :=
  generalCurvatureK J ρ a * max 0 (1 - T / Tstar)

Dependency Graph

Used by

generalKeff_zero_friction generalKeff_reduction_equal_weights generalKeff_nonneg generalKeff_above_critical generalKeff_le_standardKeff concentration_reduces_max_Keff

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:247

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