IndisputableMonolith.Cost.Jlog

   1import Mathlib
   2import Mathlib.Analysis.Complex.Trigonometric
   3
   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
  38    exact (sub_pos).2 this
  39
  40@[simp] lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by
  41  constructor
  42  · intro ht
  43    by_contra hne
  44    have : 0 < Jlog t := (Jlog_pos_iff t).2 hne
  45    linarith
  46  · intro ht
  47    subst ht
  48    simp [Jlog]
  49
  50theorem Jlog_strictMonoOn_Ici0 : StrictMonoOn Jlog (Set.Ici (0 : ℝ)) := by
  51  intro x hx y hy hxy
  52  -- strict monotonicity inherits from `cosh` on `Ici 0`
  53  have hcosh : Real.cosh x < Real.cosh y :=
  54    Real.cosh_strictMonoOn hx hy hxy
  55  -- subtracting 1 preserves strict inequality
  56  -- rewrite the goal using `Jlog = cosh - 1`
  57  rw [Jlog_eq_cosh_sub_one, Jlog_eq_cosh_sub_one]
  58  exact sub_lt_sub_right hcosh 1
  59
  60end Cost
  61end IndisputableMonolith
  62