Documentation

Lean 4 Proof

def hysteresisWidth (ρ : ℝ) (benefit_factor : ℝ) : ℝ :=
  (1 - ρ) * benefit_factor

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:66

Module Section

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

In the same file