max_intensity

formal source

 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
 139/-- cos((2n+1)π/2) = 0 for any integer n. -/
 140private lemma cos_half_odd_mul_pi (n : ℤ) : Real.cos ((2 * n + 1) * π / 2) = 0 := by
 141  have h : (2 * n + 1) * π / 2 = π / 2 + n * π := by ring
 142  rw [h, Real.cos_add, Real.cos_pi_div_two, Real.sin_pi_div_two]