`Jlog`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.Jlog
domain: Cost
line: 7 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.Jlog on GitHub at line 7.

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

   4namespace IndisputableMonolith
   5namespace Cost
   6
   7noncomputable def Jlog (t : ℝ) : ℝ := ((Real.exp t + Real.exp (-t)) / 2) - 1
   8
   9@[simp] lemma Jlog_as_exp (t : ℝ) : Jlog t = ((Real.exp t + Real.exp (-t)) / 2) - 1 := rfl
  10
  11@[simp] lemma Jlog_zero : Jlog 0 = 0 := by
  12  simp [Jlog]
  13
  14open Complex
  15
  16@[simp] lemma Jlog_eq_cosh_sub_one (t : ℝ) : Jlog t = Real.cosh t - 1 := by
  17  -- `Real.cosh_eq` gives `cosh t = (exp t + exp (-t))/2`.
  18  -- Rewrite the RHS in terms of `exp` and close by reflexivity.
  19  unfold Jlog
  20  rw [Real.cosh_eq t]
  21
  22/-! ## Basic order facts (used in "cost ⇒ atomicity" bridges) -/
  23
  24@[simp] lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t := by
  25  -- rewrite to `0 ≤ cosh t - 1` and discharge via `1 ≤ cosh t`
  26  rw [Jlog_eq_cosh_sub_one]
  27  exact sub_nonneg.mpr (Real.one_le_cosh t)
  28
  29@[simp] lemma Jlog_pos_iff (t : ℝ) : 0 < Jlog t ↔ t ≠ 0 := by
  30  -- rewrite to `0 < cosh t - 1` and use `one_lt_cosh`
  31  rw [Jlog_eq_cosh_sub_one]
  32  constructor
  33  · intro ht
  34    have : (1 : ℝ) < Real.cosh t := (sub_pos).1 ht
  35    exact (Real.one_lt_cosh (x := t)).1 this
  36  · intro hne
  37    have : (1 : ℝ) < Real.cosh t := (Real.one_lt_cosh (x := t)).2 hne

papers checked against this theorem

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