Sections / Section 13: Hierarchical Architecture / weightedNgmEntry

Weighted NGM Entry

noncomputable defprovedHierarchy

Documentation

Lean 4 Proof

noncomputable def weightedNgmEntry
    (e : WeightedHierarchicalCESEconomy N) (n : Fin N) (hn : 0 < n.val) : ℝ :=
  ngmEntry e.toHierarchicalCESEconomy n hn

Dependency Graph

Used by

weightedNgmEntry_pos

Location

thesis/CESProofs/Hierarchy/Defs.lean:328

Module Section

## Weighted Hierarchical CES Economy

In the same file

HierarchicalCESEconomy convergenceSpeed convergenceSpeed_pos ngmEntry ngmEntry_pos cycleProductBeta cycleProductBeta_pos welfareDistanceFn welfareDistanceFn_at_one welfareDistanceFn_nonneg welfareDistanceFn_eq_zero_iff welfareDistanceFn_strictly_convex treeCoefficient institutionalQuality institutionalQuality_pos welfareContribution welfareContribution_nonneg logisticElasticity logisticElasticity_zero logisticElasticity_half