`Jlog_eq_zero_iff`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.Jlog on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

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