pith. machine review for the scientific record. sign in
lemma proved tactic proof

Jlog_eq_zero_iff

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)

 296lemma Jlog_eq_zero_iff (t : ℝ) : Jlog t = 0 ↔ t = 0 := by

proof body

Tactic-mode proof.

 297  constructor
 298  · intro h
 299    have hxpos : 0 < Real.exp t := Real.exp_pos t
 300    have hxne : Real.exp t ≠ 0 := ne_of_gt hxpos
 301    have hrepr := Jcost_eq_sq hxne
 302    rw [Jlog, hrepr] at h
 303    have hden_pos : 0 < 2 * Real.exp t := by
 304      apply mul_pos
 305      · norm_num
 306      · exact hxpos
 307    have hden_ne : 2 * Real.exp t ≠ 0 := ne_of_gt hden_pos
 308    rw [div_eq_zero_iff] at h
 309    cases h with
 310    | inl h_num =>
 311      have hexp1 : Real.exp t - 1 = 0 := by nlinarith [sq_nonneg (Real.exp t - 1)]
 312      have hexp_eq : Real.exp t = 1 := by linarith
 313      rw [Real.exp_eq_one_iff] at hexp_eq
 314      exact hexp_eq
 315    | inr h_den =>
 316      exact absurd h_den hden_ne
 317  · intro h
 318    rw [h]
 319    exact Jlog_zero
 320
 321

used by (5)

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

depends on (9)

Lean names referenced from this declaration's body.