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

Adjustment Timescale At Zero

theoremprovedCES Potential

Documentation

Lean 4 Proof

theorem adjustmentTimescale_at_zero {τ₀ Tstar : ℝ} (_hTs : 0 < Tstar) :
    adjustmentTimescale τ₀ 0 Tstar = τ₀ := by
  simp [adjustmentTimescale]

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:232

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

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