Documentation

Lean 4 Proof

theorem ngmEntry_uniform_sigma (e : HierarchicalCESEconomy N) (n : Fin N) (hn : 0 < n.val)
    (hunif : ∀ m, e.sigma m = e.sigma ⟨0, by omega⟩) :
    ngmEntry e n hn = e.beta n * ↑(e.J n) * e.Fbar n := by
  simp only [ngmEntry]
  rw [hunif n, hunif ⟨n.val - 1, by omega⟩]
  have hsne : e.sigma ⟨0, by omega⟩ ≠ 0 := ne_of_gt (e.hsigma ⟨0, by omega⟩)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Defs.lean:287

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file