intensity

formal source

 100
 101/-- The intensity (probability) at point y.
 102    I(y) = |A(y)|² = 2 + 2cos(Δφ) = 4cos²(Δφ/2) -/
 103noncomputable def intensity (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
 104  let Δφ := phaseDifference setup y
 105  4 * (Real.cos (Δφ / 2))^2
 106
 107/-- **THEOREM**: Intensity oscillates with cos². -/
 108theorem intensity_oscillates (setup : DoubleSlitSetup) (y : ℝ) :
 109    intensity setup y = 4 * (Real.cos (phaseDifference setup y / 2))^2 := rfl
 110
 111/-- **THEOREM**: Maximum intensity is 4 (constructive interference). -/
 112theorem max_intensity (setup : DoubleSlitSetup) :
 113    intensity setup 0 = 4 := by
 114  unfold intensity phaseDifference pathDifference
 115  simp [Real.cos_zero]
 116
 117/-! ## Fringe Spacing -/
 118
 119/-- The fringe spacing (distance between bright fringes).
 120    Δy = λL / d -/
 121noncomputable def fringeSpacing (setup : DoubleSlitSetup) : ℝ :=
 122  setup.lambda * setup.L / setup.d
 123
 124/-! ### Helper lemmas for interference proofs -/
 125
 126/-- (-1)^n squared is 1 for any integer n. -/
 127private lemma neg_one_zpow_sq (n : ℤ) : ((-1 : ℝ) ^ n) ^ 2 = 1 := by
 128  have h : (-1 : ℝ) * (-1 : ℝ) = 1 := by norm_num
 129  calc ((-1 : ℝ) ^ n) ^ 2 = ((-1 : ℝ) ^ n * (-1 : ℝ) ^ n) := sq _
 130    _ = ((-1 : ℝ) * (-1 : ℝ)) ^ n := (mul_zpow (-1) (-1) n).symm
 131    _ = 1 ^ n := by rw [h]
 132    _ = 1 := one_zpow n
 133