lambda_PBM

formal source

 139    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
 140
 141/-- Therapeutic wavelength: λ_PBM = hc / E_PBM (meters). -/
 142noncomputable def lambda_PBM : ℝ := planck_h * speed_of_light / E_PBM
 143
 144lemma lambda_PBM_pos : 0 < lambda_PBM := by
 145  unfold lambda_PBM
 146  exact div_pos (mul_pos planck_h_pos speed_of_light_pos) E_PBM_pos
 147
 148/-- λ_PBM falls in the therapeutic photobiomodulation window (750–780 nm). -/
 149theorem lambda_PBM_in_therapeutic_window :
 150    750e-9 < lambda_PBM ∧ lambda_PBM < 780e-9 := by
 151  unfold lambda_PBM
 152  have h_hc_pos : 0 < planck_h * speed_of_light :=
 153    mul_pos planck_h_pos speed_of_light_pos
 154  have ⟨h_lower, h_upper⟩ := div_bounds_of_E_PBM h_hc_pos
 155  constructor
 156  · calc (750e-9 : ℝ)
 157        < planck_h * speed_of_light / (1.62 * eV_to_J) := by
 158          norm_num [planck_h, speed_of_light, eV_to_J]
 159      _ < planck_h * speed_of_light / E_PBM := h_lower
 160  · calc planck_h * speed_of_light / E_PBM
 161        < planck_h * speed_of_light / (1.61 * eV_to_J) := h_upper
 162      _ < (780e-9 : ℝ) := by norm_num [planck_h, speed_of_light, eV_to_J]
 163
 164/-- Tighter approximation: λ_PBM ≈ 766 nm (within ±5 nm). -/
 165theorem lambda_PBM_approx : abs (lambda_PBM - 766e-9) < 5e-9 := by
 166  unfold lambda_PBM
 167  have h_hc_pos : 0 < planck_h * speed_of_light :=
 168    mul_pos planck_h_pos speed_of_light_pos
 169  have ⟨h_lower, h_upper⟩ := div_bounds_of_E_PBM h_hc_pos
 170  have h_lo_ref :
 171      (761e-9 : ℝ) < planck_h * speed_of_light / (1.62 * eV_to_J) := by
 172    norm_num [planck_h, speed_of_light, eV_to_J]