dAlembert_diff_square

formal source

 136      _ = (2 * (H t)^2 - 1) + (2 * (H u)^2 - 1) := by simp [h2t, h2u]
 137  linarith
 138
 139lemma dAlembert_diff_square
 140  (H : ℝ → ℝ)
 141  (h_one : H 0 = 1)
 142  (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
 143  ∀ t u,
 144    (H (t+u) - H (t-u))^2 = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by
 145  intro t u
 146  have h_sum : H (t+u) + H (t-u) = 2 * H t * H u := h_dAlembert t u
 147  have h_prod : H (t+u) * H (t-u) = (H t)^2 + (H u)^2 - 1 :=
 148    dAlembert_product H h_one h_dAlembert t u
 149  calc
 150    (H (t+u) - H (t-u))^2
 151        = (H (t+u) + H (t-u))^2 - 4 * (H (t+u) * H (t-u)) := by ring
 152    _ = (2 * H t * H u)^2 - 4 * ((H t)^2 + (H u)^2 - 1) := by
 153      simp [h_sum, h_prod]
 154    _ = 4 * ((H t)^2 - 1) * ((H u)^2 - 1) := by ring
 155
 156def HasLogCurvature (H : ℝ → ℝ) (κ : ℝ) : Prop :=
 157  Filter.Tendsto (fun t => 2 * (H t - 1) / t^2) (nhds 0) (nhds κ)
 158
 159lemma sub_one_eq_mul_ratio (H : ℝ → ℝ) (h_one : H 0 = 1) (t : ℝ) :
 160  H t - 1 = (t^2 / 2) * (2 * (H t - 1) / t^2) := by
 161  by_cases ht : t = 0
 162  · subst ht
 163    simp [h_one]
 164  · field_simp [ht]
 165
 166lemma tendsto_H_one_of_log_curvature
 167  (H : ℝ → ℝ) (h_one : H 0 = 1) {κ : ℝ} (h_calib : HasLogCurvature H κ) :
 168  Filter.Tendsto H (nhds 0) (nhds 1) := by
 169  have h_t : Filter.Tendsto (fun t : ℝ => t) (nhds 0) (nhds (0 : ℝ)) := by