Weighted N Sector Economy

structure proved Dynamics & Crises

Documentation

Lean 4 Proof

structure WeightedNSectorEconomy (N : ℕ) extends NSectorEconomy N where
  /-- Per-sector weight vectors: a_n : Fin J_n → ℝ -/
  a : (n : Fin N) → Fin (toNSectorEconomy.J n) → ℝ
  /-- Weights are positive -/
  ha_pos : ∀ n j, 0 < a n j
  /-- Weights sum to 1 per sector -/
  ha_sum : ∀ n, ∑ j, a n j = 1

Dependency Graph

Used by

herfindahlAdjustedRho active_dynamics_iff_nondegen_weights sectorGeneralEffectiveCurvature sectorGeneralCurvature_pos knockout_triggered_regime_shift multi_modal_relaxation_spectrum mode_dependent_critical_frictions multi_scale_early_warning weighted_vri weighted_oscillation_spectrum sectorGeneralCurvature_le_standard sectorHerfindahl sectorGeneralCurvature dynamic_knockout_propagation equal_weight_single_relaxation coupled_rho_weights_friction_dynamics concentration_skews_variance

Location

thesis/CESProofs/Dynamics/Defs.lean:229

Module Section

## Weighted N-Sector Economy