Sections / Section 11: Dynamics and Business Cycles / varianceAtFriction

Variance Divergence

defprovedDynamics & Crises

Documentation

Lean 4 Proof

def varianceAtFriction (sigma0_sq T Tstar : ℝ) : ℝ :=
  sigma0_sq / (1 - T / Tstar)

Dependency Graph

Used by

intensification_rate variance_monotone variance_divergence susceptibility_exponent_one variance_implies_margin_floor

Location

thesis/CESProofs/Dynamics/FluctuationResponse.lean:154

Module Section

Results 8-16: Variance-Response Identity and Early Warning

In the same file

static_vri static_vri_cross sector_vri dynamic_vri T_measurement_vri autocorr_divergence autocorr_monotone variance_divergence variance_monotone recovery_divergence early_warning_signals intensification_rate weighted_vri vri_consistency_test friction_from_vri concentration_skews_variance