pith. machine review for the scientific record. sign in
def

Jcost

definition
show as:
view math explainer →
module
IndisputableMonolith.Cost
domain
Cost
line
6 · github
papers citing
33 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost on GitHub at line 6.

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

formal source

   3namespace IndisputableMonolith
   4namespace Cost
   5
   6noncomputable def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
   7
   8structure CostRequirements (F : ℝ → ℝ) : Prop where
   9  symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
  10  unit0 : F 1 = 0
  11
  12lemma Jcost_unit0 : Jcost 1 = 0 := by
  13  simp [Jcost]
  14
  15/-- J(x) expressed as a squared ratio: J(x) = (x-1)²/(2x). -/
  16lemma Jcost_eq_sq {x : ℝ} (hx : x ≠ 0) :
  17    Jcost x = (x - 1) ^ 2 / (2 * x) := by
  18  unfold Jcost
  19  field_simp [hx]
  20  ring
  21
  22lemma Jcost_symm {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹ := by
  23  have hx0 : x ≠ 0 := ne_of_gt hx
  24  rw [Jcost_eq_sq hx0, Jcost_eq_sq (inv_ne_zero hx0)]
  25  field_simp [hx0]
  26  ring
  27
  28/-- J(x) ≥ 0 for positive x (AM-GM inequality) -/
  29lemma Jcost_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ Jcost x := by
  30  have hx0 : x ≠ 0 := hx.ne'
  31  rw [Jcost_eq_sq hx0]
  32  positivity
  33
  34def AgreesOnExp (F : ℝ → ℝ) : Prop := ∀ t : ℝ, F (Real.exp t) = Jcost (Real.exp t)
  35
  36@[simp] lemma Jcost_exp (t : ℝ) :

papers checked against this theorem (showing 30 of 33)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.