def definition def or abbrev

`lambda_point`

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

formal statement (Lean)

  51noncomputable def lambda_point (T_BEC a_s n : ℝ) : ℝ :=

Definition body.

  52  T_BEC * (1 - 0.43 * a_s * n ^ ((1:ℝ)/3))
  53
  54/-- λ-point < T_BEC when interaction correction < 1. -/

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.

correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use