def definition def or abbrev

`pathLength2`

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

formal statement (Lean)

  80noncomputable def pathLength2 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=

Definition body.

  81  Real.sqrt (setup.L^2 + (y + setup.d/2)^2)
  82
  83/-- Path length difference (small angle approximation). -/

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

Lean names referenced from this declaration's body.