Documentation

Lean 4 Proof

theorem weightedCycleProductBeta_pos
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N) :
    0 < weightedCycleProductBeta e := by
  unfold weightedCycleProductBeta
  exact cycleProductBeta_pos e.toHierarchicalCESEconomy

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Defs.lean:373

Module Section

## Weighted Hierarchical CES Economy

In the same file