IndisputableMonolith.Foundation.LogicRealTranscendentals

   1import Mathlib
   2import IndisputableMonolith.Foundation.RealsFromLogic
   3
   4/-!
   5  LogicRealTranscendentals.lean
   6
   7  Transported transcendental functions on `LogicReal`.
   8
   9  The recovered real line is equivalent to Mathlib's `ℝ` by
  10  `LogicReal.equivReal`.  This module defines the standard transcendental
  11  functions by transport through that equivalence and proves the corresponding
  12  transport lemmas.  This is the right first layer: later modules can reason
  13  over `LogicReal` while still reducing analytic identities to Mathlib's
  14  established real-analysis library.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace LogicRealTranscendentals
  20
  21open RealsFromLogic RealsFromLogic.LogicReal
  22
  23noncomputable section
  24
  25/-- Square root on recovered reals, transported from `Real.sqrt`. -/
  26def sqrtL (x : LogicReal) : LogicReal := fromReal (Real.sqrt (toReal x))
  27
  28/-- Exponential on recovered reals, transported from `Real.exp`. -/
  29def expL (x : LogicReal) : LogicReal := fromReal (Real.exp (toReal x))
  30
  31/-- Natural logarithm on recovered reals, transported from `Real.log`. -/
  32def logL (x : LogicReal) : LogicReal := fromReal (Real.log (toReal x))
  33
  34/-- Real power on recovered reals, transported from `Real.rpow`. -/
  35def rpowL (x y : LogicReal) : LogicReal := fromReal (Real.rpow (toReal x) (toReal y))
  36
  37/-- The recovered constant π. -/
  38def piL : LogicReal := fromReal Real.pi
  39
  40/-- Sine on recovered reals. -/
  41def sinL (x : LogicReal) : LogicReal := fromReal (Real.sin (toReal x))
  42
  43/-- Cosine on recovered reals. -/
  44def cosL (x : LogicReal) : LogicReal := fromReal (Real.cos (toReal x))
  45
  46/-- Hyperbolic sine on recovered reals. -/
  47def sinhL (x : LogicReal) : LogicReal := fromReal (Real.sinh (toReal x))
  48
  49/-- Hyperbolic cosine on recovered reals. -/
  50def coshL (x : LogicReal) : LogicReal := fromReal (Real.cosh (toReal x))
  51
  52@[simp] theorem toReal_sqrtL (x : LogicReal) :
  53    toReal (sqrtL x) = Real.sqrt (toReal x) :=
  54  toReal_fromReal _
  55
  56@[simp] theorem toReal_expL (x : LogicReal) :
  57    toReal (expL x) = Real.exp (toReal x) :=
  58  toReal_fromReal _
  59
  60@[simp] theorem toReal_logL (x : LogicReal) :
  61    toReal (logL x) = Real.log (toReal x) :=
  62  toReal_fromReal _
  63
  64@[simp] theorem toReal_rpowL (x y : LogicReal) :
  65    toReal (rpowL x y) = Real.rpow (toReal x) (toReal y) :=
  66  toReal_fromReal _
  67
  68@[simp] theorem toReal_piL : toReal piL = Real.pi :=
  69  toReal_fromReal _
  70
  71@[simp] theorem toReal_sinL (x : LogicReal) :
  72    toReal (sinL x) = Real.sin (toReal x) :=
  73  toReal_fromReal _
  74
  75@[simp] theorem toReal_cosL (x : LogicReal) :
  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. -/
 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
 119end Foundation
 120end IndisputableMonolith
 121