  58theorem old_value_differs : 0.877 - proton_radius_codata > 0.03 := by norm_num
  59
  60/-- RS form factor correction from standard dipole. -/
  61noncomputable def form_factor_correction (Q L : ℝ) : ℝ :=
  62  1 - 0.15 * (Q / L)^2
  63
  64theorem form_factor_near_one {Q L : ℝ} (hL : 0 < L) (h : (Q/L)^2 ≤ 0.01) :
  65    |form_factor_correction Q L - 1| ≤ 0.0015 := by
  66  unfold form_factor_correction
  67  have hnn : 0 ≤ 0.15 * (Q / L)^2 := by positivity
  68  rw [show 1 - 0.15 * (Q / L)^2 - 1 = -(0.15 * (Q / L)^2) from by ring]
  69  rw [abs_neg, abs_of_nonneg hnn]
  70  nlinarith
  71
  72end ProtonRadius
  73end Physics
  74end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.