phi

formal source

  47/-! ## The auxiliary function φ -/
  48
  49/-- φ(t) = H(t) + √(H(t)² - 1) for d'Alembert solutions with H(t) ≥ 1. -/
  50def phi (H : ℝ → ℝ) (t : ℝ) : ℝ :=
  51  H t + Real.sqrt (H t ^ 2 - 1)
  52
  53/-- φ(0) = 1 when H(0) = 1. -/
  54theorem phi_at_zero (H : ℝ → ℝ) (h_one : H 0 = 1) : phi H 0 = 1 := by
  55  simp [phi, h_one]
  56
  57/-- φ(t) > 0 when H(t) ≥ 1. -/
  58theorem phi_pos (H : ℝ → ℝ) (t : ℝ) (ht : 1 ≤ H t) : 0 < phi H t := by
  59  unfold phi
  60  have h_sq : 0 ≤ H t ^ 2 - 1 := by nlinarith
  61  have h_sqrt : 0 ≤ Real.sqrt (H t ^ 2 - 1) := Real.sqrt_nonneg _
  62  linarith
  63
  64/-- H(t) can be recovered from φ: H(t) = (φ(t) + φ(t)⁻¹) / 2 when φ(t) > 0. -/
  65theorem H_from_phi (H : ℝ → ℝ) (t : ℝ) (ht : 1 ≤ H t) :
  66    H t = (phi H t + (phi H t)⁻¹) / 2 := by
  67  unfold phi
  68  set s := Real.sqrt (H t ^ 2 - 1)
  69  have hs_sq : s ^ 2 = H t ^ 2 - 1 := by
  70    exact Real.sq_sqrt (by nlinarith : 0 ≤ H t ^ 2 - 1)
  71  have hs_nonneg : 0 ≤ s := Real.sqrt_nonneg _
  72  have h_pos : 0 < H t + s := by linarith
  73  have h_inv : (H t + s)⁻¹ = H t - s := by
  74    have : (H t + s) * (H t - s) = 1 := by nlinarith [hs_sq]
  75    rw [eq_comm, inv_eq_of_mul_eq_one_right this]
  76  rw [h_inv]
  77  ring
  78
  79/-! ## The multiplicative Cauchy equation -/
  80