expL_pos

formal source

  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. -/
 110theorem coshL_eq_exp (x : LogicReal) :
 111    coshL x = (expL x + expL (-x)) / fromReal 2 := by
 112  rw [eq_iff_toReal_eq, toReal_coshL, toReal_div, toReal_add, toReal_expL,
 113    toReal_expL, toReal_neg, toReal_fromReal]
 114  exact Real.cosh_eq _
 115
 116end
 117
 118end LogicRealTranscendentals