Sections / Section 13: Hierarchical Architecture / eigenstructure_bridge_diagonal

Eigenstructure Bridge

theoremprovedHierarchy

Documentation

Lean 4 Proof

theorem eigenstructure_bridge_diagonal {tree_coeff : ℝ} {J : ℕ} {Fbar : ℝ} :
    institutionalQuality tree_coeff J Fbar = tree_coeff * ↑J * Fbar := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:119

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file

aggregateWelfareLoss aggregateWelfareLoss_nonneg aggregateWelfareLoss_eq_zero_iff welfare_lyapunov_dissipation lyapunov_within_level_dissipation bridge_eigenvalue bridge_W_uniform_depreciation welfare_loss_quadratic_approx levelWelfareLoss levelWelfareLoss_nonneg logistic_fragility_positive logistic_fragility_negative logistic_fragility_unbounded knockout_cascade_step knockout_cascade welfareDistanceFn_pos