`Jcost_pos_of_ne_one`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.JcostCore
domain: Cost
line: 296 · github
papers citing: 2 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.JcostCore on GitHub at line 296.

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

 293  exact hmain
 294
 295/-- J(x) > 0 for x ≠ 1 and x > 0 -/
 296lemma Jcost_pos_of_ne_one (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) : 0 < Jcost x := by
 297  have hx0 : x ≠ 0 := ne_of_gt hx
 298  rw [Jcost_eq_sq hx0]
 299  apply div_pos
 300  · have hne : (x - 1) ≠ 0 := sub_ne_zero.mpr hx1
 301    exact sq_pos_of_ne_zero hne
 302  · have h2 : (0 : ℝ) < 2 := by norm_num
 303    exact mul_pos h2 hx
 304
 305end Cost
 306end IndisputableMonolith

papers checked against this theorem (showing 2 of 2)

Human preferences train better flow-based video generators
unclear · 2501.13918

"Experimental results indicate that VideoReward significantly outperforms existing reward models..."
K-sparse autoencoders scale cleanly to 16 million latents
echoes · 2406.04093

"We propose using k-sparse autoencoders [Makhzani and Frey, 2013] to directly control sparsity, simplifying tuning and improving the reconstruction-sparsity frontier."