Documentation

Lean 4 Proof

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

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:305

Module Section

## Weighted Hierarchical CES Economy

In the same file