intensity_oscillates

formal source

 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
 134/-- cos(nπ)² = 1 for any integer n. -/
 135private lemma cos_int_mul_pi_sq (n : ℤ) : Real.cos (n * π) ^ 2 = 1 := by
 136  rw [Real.cos_int_mul_pi]
 137  exact neg_one_zpow_sq n
 138