`logL`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicRealTranscendentals
domain: Foundation
line: 32 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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 _

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.