`Jlog_zero`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost on GitHub at line 231.

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

 228Import `IndisputableMonolith.Cost.Convexity` to access this theorem.
 229-/
 230
 231@[simp] lemma Jlog_zero : Jlog 0 = 0 := by
 232  simp [Jlog, Jcost]
 233
 234lemma Jlog_nonneg (t : ℝ) : 0 ≤ Jlog t :=
 235  Jcost_nonneg (Real.exp_pos t)
 236
 237/-- J(x) > 0 for x ≠ 1 and x > 0. -/
 238lemma Jcost_pos_of_ne_one (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) : 0 < Jcost x := by
 239  have hx0 : x ≠ 0 := ne_of_gt hx
 240  rw [Jcost_eq_sq hx0]
 241  apply div_pos
 242  · have hne : (x - 1) ≠ 0 := sub_ne_zero.mpr hx1
 243    exact sq_pos_of_ne_zero hne
 244  · have h2 : (0 : ℝ) < 2 := by norm_num
 245    exact mul_pos h2 hx
 246
 247/-- J(x) = 0 iff x = 1, for positive x. -/
 248lemma Jcost_eq_zero_iff (x : ℝ) (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
 249  constructor
 250  · intro h
 251    by_contra h1
 252    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx h1))
 253  · intro h
 254    rw [h]
 255    exact Jcost_unit0
 256
 257/-- **THEOREM**: Jcost is surjective onto [0, ∞). -/
 258theorem Jcost_surjective_on_nonneg : ∀ y : ℝ, 0 ≤ y → ∃ x : ℝ, 1 ≤ x ∧ Jcost x = y := by
 259  intro y hy
 260  -- J(x) = (x + 1/x)/2 - 1
 261  -- Solve (x + 1/x)/2 - 1 = y => x + 1/x = 2(y+1)

papers checked against this theorem

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