Documentation

Lean 4 Proof

theorem ngmEntry_pos (e : HierarchicalCESEconomy N) (n : Fin N) (hn : 0 < n.val) :
    0 < ngmEntry e n hn := by
  simp only [ngmEntry]
  apply div_pos
  · apply mul_pos (mul_pos (mul_pos (e.hbeta n) (e.hsigma n))
      (Nat.cast_pos.mpr (by have := e.hJ n; omega))) (e.hFbar n)
  · exact e.hsigma ⟨n.val - 1, by omega⟩

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/Defs.lean:88

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file