`Jlog`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.FlogEL
domain: Cost
line: 8 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.FlogEL on GitHub at line 8.

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

   5namespace Cost
   6
   7/-- Log-domain cost: Jcost composed with exp -/
   8noncomputable def Jlog (t : ℝ) : ℝ := Jcost (Real.exp t)
   9
  10lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
  11  simp [Jlog, Jcost_unit0]
  12  have h : Real.exp t = 1 ↔ t = 0 := Real.exp_eq_one_iff
  13  exact h
  14
  15lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t := by
  16  simp [Jlog]
  17  -- Jcost is nonnegative: for x > 0, by AM-GM: x + 1/x ≥ 2, so 1/2(x + 1/x) - 1 ≥ 0
  18  have hx : 0 < Real.exp t := Real.exp_pos t
  19  have hamgm : Real.exp t + (Real.exp t)⁻¹ ≥ 2 := by
  20    have := Real.add_ge_two_mul_sqrt (Real.exp t) (Real.exp t)⁻¹
  21    · simp at this; exact this
  22    · exact hx
  23    · have : 0 < (Real.exp t)⁻¹ := inv_pos.mpr hx
  24      exact this
  25  calc
  26    Jcost (Real.exp t) = (1/2) * (Real.exp t + (Real.exp t)⁻¹) - 1 := rfl
  27    _ ≥ (1/2) * 2 - 1 := mul_le_mul_of_nonneg_left hamgm (by norm_num)
  28    _ = 0 := by norm_num
  29
  30lemma hasDerivAt_Jlog (t : ℝ) : HasDerivAt Jlog (Real.sinh t) t := by
  31  -- Jlog(t) = Jcost (exp t) = (exp t + exp (-t))/2 - 1 = cosh t - 1
  32  have hcosh : HasDerivAt Real.cosh (Real.sinh t) t := Real.hasDerivAt_cosh t
  33  have h : HasDerivAt (fun s => Real.cosh s - 1) (Real.sinh t) t := hcosh.sub_const 1
  34  -- Identify Jlog with cosh − 1 pointwise
  35  have heq : (fun s => Jlog s) = (fun s => Real.cosh s - 1) := by
  36    funext s
  37    unfold Jlog
  38    -- Jcost (exp s) = ((exp s) + (exp s)⁻¹)/2 - 1 and (exp s)⁻¹ = exp (−s)

papers checked against this theorem

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