Sections / Section 13: Hierarchical Architecture / weightedCycleProductBeta

Weighted Cycle Product Beta

noncomputable defprovedHierarchy

Documentation

Lean 4 Proof

noncomputable def weightedCycleProductBeta (e : WeightedHierarchicalCESEconomy N) : ℝ :=
  cycleProductBeta e.toHierarchicalCESEconomy

Dependency Graph

Used by

weightedCycleProductBeta_pos activation_threshold_with_weights cross_level_amplification_with_weights

Location

thesis/CESProofs/Hierarchy/Defs.lean:333

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