Variance Gap

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def varianceGap (S₀ M sig_new : ℝ) (n : ℕ) : ℝ :=
  (S₀ - M * sig_new) * (1 - 1 / M) ^ n

Dependency Graph

Used by

variance_gap_shrinks

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:133

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file

variance_decay_nonneg decay_factor_in_unit variance_decay_monotone varianceRecurrence steady_state_variance steady_state_unique steadyStateSusceptibility susceptibility_proportional_to_M variance_gap_shrinks pure_collapse_steady_state pure_collapse_susceptibility minimum_information_sources double_jeopardy