pathPhase

formal source

  69
  70/-- The phase accumulated along a path of length r.
  71    φ = 2π × r / λ = k × r (where k = 2π/λ) -/
  72noncomputable def pathPhase (r lambda : ℝ) : ℝ :=
  73  2 * π * r / lambda
  74
  75/-- Path length from source through slit 1 to point y on screen. -/
  76noncomputable def pathLength1 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  77  Real.sqrt (setup.L^2 + (y - setup.d/2)^2)
  78
  79/-- Path length from source through slit 2 to point y on screen. -/
  80noncomputable def pathLength2 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  81  Real.sqrt (setup.L^2 + (y + setup.d/2)^2)
  82
  83/-- Path length difference (small angle approximation). -/
  84noncomputable def pathDifference (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  85  -- In small angle approximation: Δr ≈ d × sin(θ) ≈ d × y / L
  86  setup.d * y / setup.L
  87
  88/-- Phase difference between the two paths. -/
  89noncomputable def phaseDifference (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  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φ₂} -/
  96noncomputable def amplitude (setup : DoubleSlitSetup) (y : ℝ) : ℂ :=
  97  let φ1 := pathPhase (pathLength1 setup y) setup.lambda
  98  let φ2 := pathPhase (pathLength2 setup y) setup.lambda
  99  Complex.exp (I * φ1) + Complex.exp (I * φ2)
 100
 101/-- The intensity (probability) at point y.
 102    I(y) = |A(y)|² = 2 + 2cos(Δφ) = 4cos²(Δφ/2) -/