Documentation

Lean 4 Proof

def ngmEntry (e : HierarchicalCESEconomy N) (n : Fin N) (hn : 0 < n.val) : ℝ :=
  e.beta n * e.sigma n * ↑(e.J n) * e.Fbar n / e.sigma ⟨n.val - 1, by omega⟩

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:84

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file