def
definition
def or abbrev
SchwarzschildMetric
show as:
view Lean formalization →
formal statement (Lean)
35noncomputable def SchwarzschildMetric (M : ℝ) : StaticSphericalMetric :=
proof body
Definition body.
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. -/