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

General Sub Critical

defprovedCES Potential

Documentation

Lean 4 Proof

def GeneralSubCritical (T Tstar : ℝ) : Prop := T < Tstar

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:292

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