theorem
proved
tactic proof
cosh_gt_one_plus_half_sq
show as:
view Lean formalization →
formal statement (Lean)
113theorem cosh_gt_one_plus_half_sq (t : ℝ) (ht : t ≠ 0) :
114 t ^ 2 / 2 < Real.cosh t - 1 := by
proof body
Tactic-mode proof.
115 have hkey : Real.cosh t - 1 = 2 * Real.sinh (t / 2) ^ 2 := by
116 have h := Real.cosh_two_mul (t / 2)
117 rw [show 2 * (t / 2) = t from by ring] at h
118 linarith [Real.cosh_sq (t / 2)]
119 rw [hkey, show t ^ 2 / 2 = 2 * (t / 2) ^ 2 from by ring]
120 have h_ne : t / 2 ≠ 0 := div_ne_zero ht two_ne_zero
121 set d := Real.cosh (t / 2) - 1 with hd_def
122 have hd_ge : (t / 2) ^ 2 / 2 ≤ d := cosh_ge_one_plus_half_sq (t / 2)
123 have hd_pos : 0 < d := by
124 have := J_log_pos h_ne; simp only [J_log] at this; linarith
125 have h_sinh_eq : Real.sinh (t / 2) ^ 2 = d ^ 2 + 2 * d := by
126 have h_cs := Real.cosh_sq (t / 2)
127 have h_cosh_eq : Real.cosh (t / 2) = d + 1 := by linarith
128 nlinarith [h_cs, sq_nonneg d]
129 nlinarith [h_sinh_eq, sq_pos_of_pos hd_pos, hd_ge]
130
131/-! ## §3. Enhancement properties -/
132
133/-- The enhancement is at least 1 for all t. -/