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
40 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost on GitHub at line 6.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

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 40)

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.