solution_exists

proof body

Tactic-mode proof.

  69  use SchwarzschildMetric M, { psi := fun _ => 0 }
  70  unfold BoundaryConditions SchwarzschildMetric
  71  constructor
  72  · -- Limit of 1 - 2M/r as r -> inf is 1
  73    intro ε hε
  74    use 2 * |M| / ε + 1
  75    intro r hr
  76    have : r > 0 := by linarith [abs_nonneg M]
  77    simp
  78    -- |(1 - 2M/r) - 1| = |2M/r| = 2|M|/r < ε
  79    rw [abs_div, abs_of_pos this]
  80    apply div_lt_of_lt_mul
  81    · linarith
  82    · linarith
  83  · -- Limit of 1 / (1 - 2M/r) as r -> inf is 1
  84    intro ε hε
  85    -- Choose R such that 2M/r < 1/2 and (1/(1-x) - 1) < ε
  86    use 4 * |M| * (1 + 1/ε) + 1
  87    intro r hr
  88    have hr_pos : r > 0 := by
  89      have : 4 * |M| * (1 + 1/ε) ≥ 0 := by positivity
  90      linarith
  91    have h_ratio : |2 * M / r| < 1 / 2 := by
  92      rw [abs_div, abs_of_pos hr_pos, div_lt_iff hr_pos]
  93      have : 4 * |M| * (1 + 1/ε) + 1 > 4 * |M| := by
  94        have : 4 * |M| / ε ≥ 0 := by positivity
  95        linarith
  96      have : r > 4 * |M| := by linarith
  97      linarith [abs_of_pos hr_pos]
  98
  99    simp only [sub_add_cancel, abs_sub_comm]
 100    -- |1 / (1 - 2M/r) - 1| = |(2M/r) / (1 - 2M/r)|
 101    have h_denom_pos : 1 - 2 * M / r > 1 / 2 := by
 102      have : 2 * M / r ≤ |2 * M / r| := le_abs_self _
 103      linarith
 104
 105    have h_eq : 1 / (1 - 2 * M / r) - 1 = (2 * M / r) / (1 - 2 * M / r) := by
 106      field_simp [hr_pos.ne', h_denom_pos.ne']
 107
 108    rw [h_eq, abs_div, abs_of_pos h_denom_pos]
 109    apply div_lt_of_lt_mul h_denom_pos
 110    -- We want |2M/r| < ε * (1 - 2M/r)
 111    -- |2M/r| + ε * (2M/r) < ε
 112    -- (2M/r) * (1 + ε) < ε if M > 0
 113    -- |2M/r| * (1 + ε) < ε
 114    -- 2|M|/r * (1 + ε) < ε
 115    -- 2|M|(1 + ε) / ε < r
 116    -- 2|M|(1/ε + 1) < r
 117    have h_r_bound : r > 2 * |M| * (1 / ε + 1) := by
 118      have : 4 * |M| * (1 + 1/ε) + 1 > 2 * |M| * (1 + 1/ε) := by
 119        have : 2 * |M| * (1 + 1/ε) + 1 > 0 := by positivity
 120        linarith
 121      linarith
 122
 123    rw [abs_div, abs_of_pos hr_pos]
 124    have h_goal : 2 * |M| < r * ε * (1 - 2 * M / r) := by
 125      have : r * ε * (1 - 2 * M / r) = ε * r - ε * 2 * M := by ring
 126      rw [this]
 127      -- We need 2|M| < ε*r - 2εM
 128      -- 2|M| + 2εM < ε*r
 129      -- 2|M|(1+ε) < ε*r
 130      -- 2|M|(1+ε)/ε < r
 131      -- 2|M|(1/ε + 1) < r
 132      have h_M_le : 2 * M ≤ 2 * |M| := by linarith [le_abs_self M]
 133      have : ε * 2 * M ≤ ε * 2 * |M| := (mul_le_mul_left hε).mpr h_M_le
 134      have : 2 * |M| * (1 + ε) < ε * r := by
 135        rw [mul_comm ε r, ← div_lt_iff hε]
 136        field_simp [hε.ne']
 137        linarith
 138      linarith
 139    exact h_goal
 140