Documentation

Lean 4 Proof

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

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:107

Module Section

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

In the same file