pith. machine review for the scientific record. sign in
def definition def or abbrev

phaseDifference

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  89noncomputable def phaseDifference (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=

proof body

Definition body.

  90  2 * π * pathDifference setup y / setup.lambda
  91
  92/-! ## Interference Pattern -/
  93
  94/-- The amplitude at point y is the sum of two complex amplitudes.
  95    A(y) = e^{iφ₁} + e^{iφ₂} -/

used by (5)

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

depends on (23)

Lean names referenced from this declaration's body.