pith. machine review for the scientific record. sign in
theorem proved term proof

Jlog_strictMonoOn_Ici0

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  50theorem Jlog_strictMonoOn_Ici0 : StrictMonoOn Jlog (Set.Ici (0 : ℝ)) := by

proof body

Term-mode proof.

  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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.