SchwarzschildMetric

formal source

  32    f(r) = 1 - 2M/r, g(r) = (1 - 2M/r)⁻¹ for r > 2|M|.
  33    For r ≤ 2|M|, we use a positive constant to satisfy the metric structure
  34    outside the coordinate singularity. -/
  35noncomputable def SchwarzschildMetric (M : ℝ) : StaticSphericalMetric :=
  36  { f := fun r => if r > 2 * |M| then 1 - 2 * M / r else 1
  37    g := fun r => if r > 2 * |M| then 1 / (1 - 2 * M / r) else 1
  38    f_positive := by
  39      intro r hr
  40      by_cases h_rad : r > 2 * |M|
  41      · simp [h_rad]
  42        -- 1 - 2M/r > 0  ⟺  r > 2M
  43        -- We have r > 2|M| and 2|M| ≥ 2M
  44        have h_gt : r > 2 * M := by linarith [abs_le_abs_self M, le_abs_self M]
  45        apply sub_pos.mpr
  46        rw [div_lt_one hr]
  47        linarith
  48      · simp [h_rad]
  49        norm_num
  50    g_positive := by
  51      intro r hr
  52      by_cases h_rad : r > 2 * |M|
  53      · simp [h_rad]
  54        have h_gt : r > 2 * M := by linarith [abs_le_abs_self M, le_abs_self M]
  55        apply one_div_pos.mpr
  56        apply sub_pos.mpr
  57        rw [div_lt_one hr]
  58        linarith
  59      · simp [h_rad]
  60        norm_num
  61  }
  62
  63/--- **THEOREM (GROUNDED)**: Existence of static spherical solutions.
  64    For a vacuum region outside a mass M, the Schwarzschild metric provides
  65     a stationary section of the Recognition Science action. -/