NGM Entry Real

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def ngmEntryReal (beta_n sigma_n J_n Fbar_n sigma_prev : ℝ) : ℝ :=
  beta_n * sigma_n * J_n * Fbar_n / sigma_prev

Dependency Graph

Used by

ngmEntryReal_pos J_mediated_activation_linearity upstream_reform_for_J ngmEntryReal_linear_in_J upstream_reform_beta_for_J

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:107

Module Section

## Entry-Exit Core Definitions (merged from EntryExitDefs.lean)