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

Jcost_symm

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost on GitHub at line 22.

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

  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
  43  symmetric : ∀ {x}, 0 < x → F x = F x⁻¹
  44  unit0 : F 1 = 0
  45
  46class AveragingAgree (F : ℝ → ℝ) : Prop where
  47  agrees : AgreesOnExp F
  48
  49class AveragingDerivation (F : ℝ → ℝ) : Prop extends SymmUnit F where
  50  agrees : AgreesOnExp F
  51
  52lemma even_on_log_of_symm {F : ℝ → ℝ} [SymmUnit F] (t : ℝ) :

papers checked against this theorem (showing 5 of 5)