toReal_sinhL

formal source

  76    toReal (cosL x) = Real.cos (toReal x) :=
  77  toReal_fromReal _
  78
  79@[simp] theorem toReal_sinhL (x : LogicReal) :
  80    toReal (sinhL x) = Real.sinh (toReal x) :=
  81  toReal_fromReal _
  82
  83@[simp] theorem toReal_coshL (x : LogicReal) :
  84    toReal (coshL x) = Real.cosh (toReal x) :=
  85  toReal_fromReal _
  86
  87/-- Transported positivity of exponential. -/
  88theorem expL_pos (x : LogicReal) : (0 : LogicReal) < expL x := by
  89  rw [lt_iff_toReal_lt, toReal_zero, toReal_expL]
  90  exact Real.exp_pos _
  91
  92/-- Transported non-negativity of square root. -/
  93theorem sqrtL_nonneg (x : LogicReal) : (0 : LogicReal) ≤ sqrtL x := by
  94  rw [le_iff_toReal_le, toReal_zero, toReal_sqrtL]
  95  exact Real.sqrt_nonneg _
  96
  97/-- Transported exponential/log inverse on positive recovered reals. -/
  98theorem expL_logL {x : LogicReal} (hx : (0 : LogicReal) < x) :
  99    expL (logL x) = x := by
 100  rw [eq_iff_toReal_eq, toReal_expL, toReal_logL]
 101  have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
 102  exact Real.exp_log hx'
 103
 104/-- Transported logarithm/exponential inverse. -/
 105theorem logL_expL (x : LogicReal) : logL (expL x) = x := by
 106  rw [eq_iff_toReal_eq, toReal_logL, toReal_expL]
 107  exact Real.log_exp _
 108
 109/-- Transported hyperbolic cosine definition. -/