Documentation

Lean 4 Proof

theorem ngmEntry_real_pos {beta_n sigma_n J_n Fbar_n sigma_prev : ℝ}
    (hb : 0 < beta_n) (hs : 0 < sigma_n) (hJ : 0 < J_n)
    (hF : 0 < Fbar_n) (hsp : 0 < sigma_prev) :
    0 < ngmEntry_real beta_n sigma_n J_n Fbar_n sigma_prev := by
  simp only [ngmEntry_real]
  exact div_pos (by positivity) hsp

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:111

Module Section

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

In the same file