deflection_angle_formula

formal source

  56    Derivation: null geodesic u'' + u = (3/2)r_s u² in Schwarzschild.
  57    Zeroth order: u₀ = sinφ/b.
  58    First order correction integrates to total bending 2r_s/b. -/
  59theorem deflection_angle_formula (M b : ℝ) (hM : 0 < M) (hb : 0 < b) :
  60    deflection_GR M b = 2 * schwarzschild_radius M / b := by
  61  unfold deflection_GR
  62  ring
  63
  64/-- The deflection angle is positive for positive mass and impact parameter. -/
  65theorem deflection_positive (M b : ℝ) (hM : 0 < M) (hb : 0 < b) :
  66    0 < deflection_GR M b := by
  67  unfold deflection_GR schwarzschild_radius
  68  positivity
  69
  70/-- Deflection angle scales as 1/b (stronger lensing at smaller impact). -/
  71theorem deflection_inverse_b (M b₁ b₂ : ℝ) (hM : 0 < M) (hb₁ : 0 < b₁) (hb₂ : 0 < b₂)
  72    (hb₁b₂ : b₁ < b₂) :
  73    deflection_GR M b₂ < deflection_GR M b₁ := by
  74  unfold deflection_GR schwarzschild_radius
  75  have hpos : (0 : ℝ) < 2 * (2 * M) := by linarith
  76  gcongr
  77
  78/-! ## Einstein Ring -/
  79
  80/-- **EINSTEIN RADIUS**: When source, lens, and observer are aligned,
  81    the image forms a ring of angular radius θ_E.
  82
  83    θ_E² = (4GM/c²) × D_LS / (D_L × D_S)
  84
  85    In natural units (with distances in units where G=c=1):
  86    θ_E² = (2 r_s) × D_LS / (D_L × D_S) -/
  87noncomputable def einstein_angle_sq (M DL DS DLS : ℝ) : ℝ :=
  88  schwarzschild_radius M * DLS / (DL * DS)
  89