def definition def or abbrev

`lennardJonesPotential`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  56def lennardJonesPotential (ε σ r : ℝ) : ℝ :=

Definition body.

  57  if r ≤ 0 then 0
  58  else 4 * ε * ((σ / r) ^ 12 - (σ / r) ^ 6)
  59
  60/-- The LJ potential has a minimum at r = 2^(1/6) * σ ≈ 1.122σ. -/

Lean names referenced from this declaration's body.