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

Jcost_unit0

proved
show as:
view math explainer →
module
IndisputableMonolith.Cost
domain
Cost
line
12 · github
papers citing
23 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost on GitHub at line 12.

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

   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 : ℝ) :
  37  Jcost (Real.exp t) = ((Real.exp t) + (Real.exp (-t))) / 2 - 1 := by
  38  have h : (Real.exp t)⁻¹ = Real.exp (-t) := by
  39    symm; simp [Real.exp_neg t]
  40  simp [Jcost, h]
  41
  42class SymmUnit (F : ℝ → ℝ) : Prop where

papers checked against this theorem (showing 23 of 23)