Hquad

formal source

  93
  94/-! ## The d'Alembert equation fails for the quadratic log-lift -/
  95
  96noncomputable def Hquad (t : ℝ) : ℝ := (fun t => Fquad (Real.exp t)) t + 1
  97
  98lemma Hquad_simp (t : ℝ) : Hquad t = t ^ 2 / 2 + 1 := by
  99  simp [Hquad, Fquad_on_exp, Gquad]
 100
 101theorem Hquad_not_dAlembert :
 102    ¬ (Hquad 0 = 1 ∧ ∀ t u : ℝ, Hquad (t + u) + Hquad (t - u) = 2 * Hquad t * Hquad u) := by
 103  intro h
 104  have h0 : Hquad 0 = 1 := h.1
 105  have hdA := h.2
 106  -- Evaluate the d'Alembert identity at t = 1, u = 1.
 107  have h11 := hdA 1 1
 108  -- Compute both sides explicitly; they disagree (4 ≠ 9/2).
 109  have hL : Hquad (1 + 1) + Hquad (1 - 1) = 4 := by
 110    calc
 111      Hquad (1 + 1) + Hquad (1 - 1)
 112          = ((1 + 1) ^ 2 / 2 + 1) + ((1 - 1) ^ 2 / 2 + 1) := by
 113              simp [Hquad_simp]
 114      _ = 4 := by
 115            norm_num
 116  have hR : 2 * Hquad 1 * Hquad 1 = (9 : ℝ) / 2 := by
 117    simp [Hquad_simp]
 118    ring
 119  -- Contradiction
 120  have : (4 : ℝ) = (9 : ℝ) / 2 := by
 121    calc (4 : ℝ) = Hquad (1 + 1) + Hquad (1 - 1) := by simpa using hL.symm
 122      _ = 2 * Hquad 1 * Hquad 1 := h11
 123      _ = (9 : ℝ) / 2 := hR
 124  norm_num at this
 125
 126end Counterexamples