Documentation

Lean 4 Proof

theorem weightedNgmEntry_pos
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N) (n : Fin N) (hn : 0 < n.val) :
    0 < weightedNgmEntry e n hn := by
  unfold weightedNgmEntry
  exact ngmEntry_pos e.toHierarchicalCESEconomy n hn

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Defs.lean:366

Module Section

## Weighted Hierarchical CES Economy

In the same file